From 01831775022e9ca30d2414b50e9275f2fd148555 Mon Sep 17 00:00:00 2001 From: Chris Dare Date: Thu, 3 Sep 2026 22:59:23 -0400 Subject: [PATCH 1/4] resolution/1.0 could not say "I decline to answer" (arXMCP #170) `documents.arxiv_version` is `''` for every row in both live notebooks, so a resolver that matches an entry's `quote_sha256` against corpus bytes and writes `current` for an entry declaring `version: v3` asserts a v3 pin confirmed by bytes of unknown version. derived-alg-geo-lean #170 requires the resolver to emit `not_applicable` there, and the enum had no such member. The four values this contract judges on are `pass` / `fail` / `not_run` / `not_applicable` (ADR-0005), and arXMCP's CLAUDE.md 4.10 rule 3 binds the same spelling across the seam. `join.py` already carries the constant and already states why it may not be folded into `not_run` -- the remedies differ. The corpus axis is simply its second user. Extended in place rather than bumped to `resolution/1.1`: no producer of `resolution/1.0` has ever existed. `attest/resolution.json` is absent from the topic repo and C-08 reports `not_run` in the v0.1.0 release notes, so there is no file in the world to invalidate. There will be after arXMCP #170 lands. - `result.resolution` gains `not_applicable`; `counts` gains its key. - A new conditional: `not_applicable` MUST carry a non-empty `reason`, and MUST NOT name a `resolved_source_version`. A result that both declines on version grounds and names a version is incoherent; and without the reason it is indistinguishable from `not_run` at the point of reading. - `coverage()` counted `resolution != not_run` as resolved, which would have reported the soundness hole as coverage -- exactly what the `reviewed` line next to it already refuses to do. Now excludes both, as that line does. Two rejection fixtures, both asserted at the schema and (through `test_validate.py`'s sweep of the directory) at the CLI. Also registers `containment-with-similarity.json` in `REJECTIONS`, where it never was. The directory sweep meant it was asserted to fail *somehow*, which is a weaker claim than it looks: `additionalProperties: false` rejects a document for a typo, so "the CLI said no" does not establish that the rule the fixture was written for is the rule that fired. `REJECTIONS` binds a fixture to its rule, and a new test now fails on any fixture that is in neither. And a structural test that `counts` has one key per `resolution` enum member, derived from the schema rather than listed -- an enum member with no counts key is a state every total silently swallows. 631 passed, 1 skipped (was 623, 1). --- contract/mfc/join.py | 11 ++++- .../mfc/schema/resolution-1.0.schema.json | 37 ++++++++++++++- .../invalid/not-applicable-with-version.json | 32 +++++++++++++ .../not-applicable-without-reason.json | 32 +++++++++++++ .../artifacts/valid/resolution-1.0.json | 14 +++++- contract/tests/test_join.py | 22 +++++++++ contract/tests/test_schemas.py | 46 +++++++++++++++++++ 7 files changed, 191 insertions(+), 3 deletions(-) create mode 100644 contract/testdata/artifacts/invalid/not-applicable-with-version.json create mode 100644 contract/testdata/artifacts/invalid/not-applicable-without-reason.json diff --git a/contract/mfc/join.py b/contract/mfc/join.py index 8b93dc5..da9e020 100644 --- a/contract/mfc/join.py +++ b/contract/mfc/join.py @@ -89,6 +89,14 @@ #: producer. This is the consumer's question -- given a record I did not build, #: what does it tell me about the environment I hold? -- and its answer is #: "nothing about this one". +#: +#: The review axes were its first user; the CORPUS axis is its second. +#: `resolution/1.0` gained the same value for the same reason -- a byte-equal +#: match against a corpus that records no arXiv version is no evidence for the +#: `vN` an entry pins -- so `coverage()` must exclude it from `resolved` exactly +#: as it already excludes it from `reviewed`. Counting it would restate the +#: soundness hole as a statistic, which is the failure this constant exists to +#: prevent. NOT_APPLICABLE = "not_applicable" @@ -435,7 +443,8 @@ def coverage(rows: Iterable[Row]) -> Coverage: keys=len({r.key for r in rows}), reviewed=sum(1 for r in rows if r.faithfulness not in (NOT_RUN, NOT_APPLICABLE)), - resolved=sum(1 for r in rows if r.resolution != NOT_RUN), + resolved=sum(1 for r in rows + if r.resolution not in (NOT_RUN, NOT_APPLICABLE)), frontier_open=sum(1 for r in rows if r.frontier != "-"), review_not_applicable=sum(1 for r in rows if r.faithfulness == NOT_APPLICABLE), diff --git a/contract/mfc/schema/resolution-1.0.schema.json b/contract/mfc/schema/resolution-1.0.schema.json index bdc2d78..3f12bdb 100644 --- a/contract/mfc/schema/resolution-1.0.schema.json +++ b/contract/mfc/schema/resolution-1.0.schema.json @@ -55,11 +55,13 @@ "counts": { "type": "object", "additionalProperties": false, + "$comment": "One key per member of the `resolution` enum, and `tests/test_schemas.py` asserts that correspondence structurally -- an enum member with no counts key is a state the summary silently swallows.", "required": [ "current", "drifted", "unresolvable", "paper_absent", + "not_applicable", "not_run" ], "properties": { @@ -79,6 +81,10 @@ "type": "integer", "minimum": 0 }, + "not_applicable": { + "type": "integer", + "minimum": 0 + }, "not_run": { "type": "integer", "minimum": 0 @@ -112,8 +118,10 @@ "drifted", "unresolvable", "paper_absent", + "not_applicable", "not_run" - ] + ], + "$comment": "`not_applicable` is the resolver declining to adjudicate, and it is kept apart from `not_run` because the remedies differ -- `not_run` is closed by running the resolver, `not_applicable` by fixing the corpus. It is the value ADR-0003 and ADR-0005 already name (`pass`/`fail`/`not_run`/`not_applicable`), and arXMCP's CLAUDE.md 4.10 rule 3 binds the same spelling across the seam. Its live case: `documents.arxiv_version` is '' for every row in every notebook, so a `current` verdict for an entry declaring `version: vN` would assert a vN pin confirmed by bytes of unknown version. A byte-equal match against an unversioned corpus is not weak evidence for that pin -- it is no evidence for it." }, "matched_by": { "enum": [ @@ -243,6 +251,33 @@ } } }, + { + "$comment": "`not_applicable` must SAY why it declines, and it may never name a source version. The reason is what separates it from `not_run` for a reader: one means nobody ran the resolver, the other means the resolver ran and the corpus could not answer. And `resolved_source_version` is precisely the field whose absence forces this state -- a result that both declines on version grounds and names a version is incoherent.", + "if": { + "properties": { + "resolution": { + "const": "not_applicable" + } + }, + "required": [ + "resolution" + ] + }, + "then": { + "required": [ + "reason" + ], + "properties": { + "reason": { + "type": "string", + "minLength": 1 + }, + "resolved_source_version": { + "type": "null" + } + } + } + }, { "$comment": "`quote_containment` may read `current`, and that is the whole point of the rung: containment is an IDENTITY claim -- the statement is in the chunk or it is not -- where `fuzzy` is an estimate. It still owes the same evidence as any other current result (the first conditional above), and it must carry NO similarity score: a number there would invite exactly the reading that this is a near-miss.", "if": { diff --git a/contract/testdata/artifacts/invalid/not-applicable-with-version.json b/contract/testdata/artifacts/invalid/not-applicable-with-version.json new file mode 100644 index 0000000..2f0e70f --- /dev/null +++ b/contract/testdata/artifacts/invalid/not-applicable-with-version.json @@ -0,0 +1,32 @@ +{ + "schema_version": "resolution/1.0", + "registry_sha256": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "notebook": "bridgeland-stability", + "corpus_version": 5048, + "corpus_manifest_content_hash": "1111111111111111111111111111111111111111111111111111111111111111", + "resolver_version": "arxmcp/statement_resolve.py@1.0.0", + "chunker_version": "chunker/2.3.0", + "generated_at": "2026-08-04T08:55:10Z", + "results": [ + { + "key": "stmt:9f4c1a20b7d3:bridgeland2007.def-1.1", + "resolution": "not_applicable", + "matched_by": "quote_sha256", + "chunk_id": "arxiv:math/0212237:5f1b90c2e6a4118d", + "resolved_source_version": "v3", + "matched_body_sha256": "ebacfe5caa6c1df8229ec6bfbcf55f855a524a77cf78a9fb3171b81172d6f50d", + "printed_number": "1.1", + "similarity": null, + "reason": "The quote is byte-equal to a chunk of this paper, but the entry declares source.version v3 and documents.arxiv_version is '' for every row of this notebook. Calling that `current` would assert a v3 pin confirmed by bytes of unknown version." + } + ], + "counts": { + "current": 0, + "drifted": 0, + "unresolvable": 0, + "paper_absent": 0, + "not_applicable": 1, + "not_run": 0 + }, + "$comment_fixture": "REJECTION FIXTURE. A not_applicable result that names the very version whose absence is the only reason to emit not_applicable. If the resolver could establish v3 it owed a verdict, not an abstention." +} diff --git a/contract/testdata/artifacts/invalid/not-applicable-without-reason.json b/contract/testdata/artifacts/invalid/not-applicable-without-reason.json new file mode 100644 index 0000000..bdb594d --- /dev/null +++ b/contract/testdata/artifacts/invalid/not-applicable-without-reason.json @@ -0,0 +1,32 @@ +{ + "schema_version": "resolution/1.0", + "registry_sha256": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "notebook": "bridgeland-stability", + "corpus_version": 5048, + "corpus_manifest_content_hash": "1111111111111111111111111111111111111111111111111111111111111111", + "resolver_version": "arxmcp/statement_resolve.py@1.0.0", + "chunker_version": "chunker/2.3.0", + "generated_at": "2026-08-04T08:55:10Z", + "results": [ + { + "key": "stmt:9f4c1a20b7d3:bridgeland2007.def-1.1", + "resolution": "not_applicable", + "matched_by": "quote_sha256", + "chunk_id": "arxiv:math/0212237:5f1b90c2e6a4118d", + "resolved_source_version": null, + "matched_body_sha256": "ebacfe5caa6c1df8229ec6bfbcf55f855a524a77cf78a9fb3171b81172d6f50d", + "printed_number": "1.1", + "similarity": null, + "reason": null + } + ], + "counts": { + "current": 0, + "drifted": 0, + "unresolvable": 0, + "paper_absent": 0, + "not_applicable": 1, + "not_run": 0 + }, + "$comment_fixture": "REJECTION FIXTURE. A not_applicable result that does not say why. Without the reason it is indistinguishable from not_run at the point of reading, and the two have different remedies -- not_run is closed by running the resolver, not_applicable by fixing the corpus." +} diff --git a/contract/testdata/artifacts/valid/resolution-1.0.json b/contract/testdata/artifacts/valid/resolution-1.0.json index 2ebd669..4aa4aa8 100644 --- a/contract/testdata/artifacts/valid/resolution-1.0.json +++ b/contract/testdata/artifacts/valid/resolution-1.0.json @@ -40,6 +40,17 @@ "printed_number": "8.2", "similarity": null, "reason": "The chunker merged this statement's chunk with the following one; the quote is still present, so this is current by containment rather than by byte-equality." + }, + { + "key": "stmt:9f4c1a20b7d3:bridgeland2007.def-1.1", + "resolution": "not_applicable", + "matched_by": "quote_sha256", + "chunk_id": "arxiv:math/0212237:5f1b90c2e6a4118d", + "resolved_source_version": null, + "matched_body_sha256": "ebacfe5caa6c1df8229ec6bfbcf55f855a524a77cf78a9fb3171b81172d6f50d", + "printed_number": "1.1", + "similarity": null, + "reason": "The quote is byte-equal to a chunk of this paper, but the entry declares source.version v3 and documents.arxiv_version is '' for every row of this notebook. Calling that `current` would assert a v3 pin confirmed by bytes of unknown version." } ], "counts": { @@ -47,6 +58,7 @@ "drifted": 0, "unresolvable": 0, "paper_absent": 0, - "not_run": 1 + "not_run": 1, + "not_applicable": 1 } } diff --git a/contract/tests/test_join.py b/contract/tests/test_join.py index add83d3..24daca8 100644 --- a/contract/tests/test_join.py +++ b/contract/tests/test_join.py @@ -501,6 +501,28 @@ def test_coverage_keeps_reviewed_and_resolved_apart() -> None: assert "score" not in c._fields and "ratio" not in c._fields +def test_a_not_applicable_resolution_is_not_counted_as_resolved() -> None: + """The corpus axis gets the same treatment the review axes already get. + + `coverage()` tested `!= NOT_RUN`, which was correct while `not_applicable` + could only appear on a review cell. `resolution/1.0` now carries it too -- + a byte-equal match against a corpus that records no arXiv version is no + evidence for the `vN` an entry pins -- and counting it as resolved would + report the soundness hole as coverage, which is precisely what the + `reviewed` line already refuses to do. + """ + decls = _declarations([ + _decl("Topic.a", DIGEST_A, [_cite(KEY_A)]), + _decl("Topic.b", DIGEST_B, [_cite(KEY_B)]), + ]) + c = coverage(claim_table( + decls, + resolution=_resolution(_result(KEY_A), + _result(KEY_B, resolution=NOT_APPLICABLE)), + environment=_environment())) + assert (c.bindings, c.resolved) == (2, 1) + + def test_a_declaration_citing_two_keys_yields_two_rows() -> None: decls = _declarations([_decl("Topic.thm", DIGEST_A, [_cite(KEY_A), _cite(KEY_B)])]) diff --git a/contract/tests/test_schemas.py b/contract/tests/test_schemas.py index f8b801d..c00ad8b 100644 --- a/contract/tests/test_schemas.py +++ b/contract/tests/test_schemas.py @@ -26,6 +26,12 @@ VALID_DIR = HERE.parent / "testdata" / "artifacts" / "valid" INVALID_DIR = HERE.parent / "testdata" / "artifacts" / "invalid" +#: Rejection fixtures whose assertion lives in another test module, so +#: `test_every_rejection_fixture_is_registered` does not report them as +#: unclaimed. `not-checkable-without-reason` is `restate/1.0`'s and is +#: asserted through the CLI in `tests/test_restate.py`. +_REJECTIONS_OWNED_ELSEWHERE = {"not-checkable-without-reason"} + #: Which schema each rejection fixture is aimed at, and the rule it must trip. REJECTIONS = { "sorry-laundered": ("declarations-1.0", @@ -34,6 +40,12 @@ "a fuzzy match may never be `current`"), "current-without-digest": ("resolution-1.0", "`current` requires a recomputed body digest"), + "containment-with-similarity": ("resolution-1.0", + "a containment match may carry no similarity score"), + "not-applicable-without-reason": ("resolution-1.0", + "`not_applicable` must say why it declines"), + "not-applicable-with-version": ("resolution-1.0", + "`not_applicable` may not name a resolved source version"), "exact-with-divergence": ("review-1.0", "`exact` confirmed alongside a stated divergence"), "divergent-without-divergence": ("review-1.0", @@ -130,6 +142,40 @@ def test_rejection_fixture_is_rejected(fixture: str, expected: tuple[str, str]) assert errors, f"{schema_name} accepted {fixture!r}; the rule is not firing: {rule}" +def test_every_rejection_fixture_is_registered() -> None: + """A fixture named by no rule is a fixture that proves the wrong thing. + + `test_validate.py` already parametrizes over this directory, so every file + here is asserted to FAIL the CLI. That is a weaker claim than it looks: + `additionalProperties: false` rejects any document for a typo, so "the CLI + said no" does not establish that the rule the fixture was written for is + the rule that fired. `REJECTIONS` is where a fixture is bound to its rule, + and `containment-with-similarity.json` sat outside it from the day it was + written. Registering it is the fix; this test is what stops the next one + from going the same way. + """ + on_disk = {p.stem for p in INVALID_DIR.glob("*.json")} + unclaimed = on_disk - set(REJECTIONS) - _REJECTIONS_OWNED_ELSEWHERE + assert not unclaimed, ( + f"rejection fixture(s) {sorted(unclaimed)} are asserted on by nothing") + + +def test_resolution_counts_has_one_key_per_enum_member() -> None: + """The summary must be able to express every state a result can be in. + + `counts` is how a reader learns the shape of a run without walking + `results`, so an enum member with no counts key is a state the summary + swallows: entries in it are simply missing from every total. Derived from + the schema rather than listed, so adding a member without its key fails + here instead of silently under-reporting in CI. + """ + schema = _schema("resolution-1.0") + members = set(schema["$defs"]["result"]["properties"]["resolution"]["enum"]) + counted = set(schema["properties"]["counts"]["properties"]) + assert members == counted + assert set(schema["properties"]["counts"]["required"]) == members + + def test_emission_fixture_is_real_emitter_output() -> None: """The emission fixture is trimmed real output, not hand-written. From 498bd59e7848de81d97e0916b67528c4b2814467 Mon Sep 17 00:00:00 2001 From: Chris Dare Date: Thu, 3 Sep 2026 23:05:47 -0400 Subject: [PATCH 2/4] The version guard is orthogonal to the rung that found the quote `quote_containment`'s conditional listed `current`/`drifted`/`unresolvable`, which made a containment match withheld by the version guard unrepresentable. The resolver would then have had to misreport the rung it actually used -- writing `quote_sha256` for a match it made by containment -- to say the one thing the guard requires it to say. An entry found by containment in a corpus that cannot name its arXiv version is withheld for exactly the reason a byte-equal match is. Which rung found the quote and whether the version can be confirmed are independent questions, and the schema now lets a result answer them independently. The valid fixture carries both combinations, so the accepted pairing is evidence rather than an absence of a rejection. --- contract/mfc/schema/resolution-1.0.schema.json | 5 +++-- .../testdata/artifacts/valid/resolution-1.0.json | 13 ++++++++++++- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/contract/mfc/schema/resolution-1.0.schema.json b/contract/mfc/schema/resolution-1.0.schema.json index 3f12bdb..8f71cef 100644 --- a/contract/mfc/schema/resolution-1.0.schema.json +++ b/contract/mfc/schema/resolution-1.0.schema.json @@ -279,7 +279,7 @@ } }, { - "$comment": "`quote_containment` may read `current`, and that is the whole point of the rung: containment is an IDENTITY claim -- the statement is in the chunk or it is not -- where `fuzzy` is an estimate. It still owes the same evidence as any other current result (the first conditional above), and it must carry NO similarity score: a number there would invite exactly the reading that this is a near-miss.", + "$comment": "`quote_containment` may read `current`, and that is the whole point of the rung: containment is an IDENTITY claim -- the statement is in the chunk or it is not -- where `fuzzy` is an estimate. It still owes the same evidence as any other current result (the first conditional above), and it must carry NO similarity score: a number there would invite exactly the reading that this is a near-miss. `not_applicable` is in the list because the version guard is orthogonal to the rung: an entry found by containment in a corpus that cannot name its arXiv version is withheld for the same reason one found by byte-equality is, and excluding it here would have forced the resolver to misreport the rung it actually used.", "if": { "properties": { "matched_by": { @@ -296,7 +296,8 @@ "enum": [ "current", "drifted", - "unresolvable" + "unresolvable", + "not_applicable" ] }, "similarity": { diff --git a/contract/testdata/artifacts/valid/resolution-1.0.json b/contract/testdata/artifacts/valid/resolution-1.0.json index 4aa4aa8..52b2515 100644 --- a/contract/testdata/artifacts/valid/resolution-1.0.json +++ b/contract/testdata/artifacts/valid/resolution-1.0.json @@ -51,6 +51,17 @@ "printed_number": "1.1", "similarity": null, "reason": "The quote is byte-equal to a chunk of this paper, but the entry declares source.version v3 and documents.arxiv_version is '' for every row of this notebook. Calling that `current` would assert a v3 pin confirmed by bytes of unknown version." + }, + { + "key": "stmt:9f4c1a20b7d3:bridgeland2007.def-3.3", + "resolution": "not_applicable", + "matched_by": "quote_containment", + "chunk_id": "arxiv:math/0212237:c07a41ff2b93d5e8", + "resolved_source_version": null, + "matched_body_sha256": "ebacfe5caa6c1df8229ec6bfbcf55f855a524a77cf78a9fb3171b81172d6f50d", + "printed_number": "3.3", + "similarity": null, + "reason": "Found by containment after a re-chunk merged this statement's chunk -- and withheld for the same reason the byte-equal match above is: the corpus cannot name the arXiv version it holds. The version guard is orthogonal to which rung found the quote." } ], "counts": { @@ -59,6 +70,6 @@ "unresolvable": 0, "paper_absent": 0, "not_run": 1, - "not_applicable": 1 + "not_applicable": 2 } } From 2dc77b80c0cba2c1780443384f972c0a6ba16c7c Mon Sep 17 00:00:00 2001 From: Chris Dare Date: Thu, 3 Sep 2026 23:12:23 -0400 Subject: [PATCH 3/4] `pip install ./contract` could ship a 2026-era schema `/contract/build/` is in `.gitignore` and has been since packaging landed -- but eleven files under it went in with 6bd4739, the same commit that added the ignore, and `.gitignore` does not untrack what is already tracked. So a fresh checkout carried a `build/lib/` holding stale copies of `cli.py`, `lint.py`, `validate.py` and five schemas, and setuptools' `build_py` copies a source file into `build/lib` only when it is NEWER -- which on a fresh checkout, with every file stamped at the same moment, it need not be. Not hypothetical. It bit this branch: `pip install ./contract` shipped a `resolution-1.0.schema.json` predating `not_applicable`, so a resolver producing a valid document was told by its own bundled schema that the document was invalid. Eight of the eleven tracked files were stale. CI already installs the package rather than running it from the tree, and the comment there says why -- that is what catches a schema which failed to ship. It cannot catch one that shipped as the WRONG BYTES, because from outside those two look identical. So the new test compares the installed schemas against the source schemas byte for byte, and says to delete `build/` if they differ. Byte-identity rather than parsed equality: a schema can differ by a `$comment` that changes nothing and an enum member that changes everything, and only one of those survives a structural diff. It skips when `mfc` resolves to the source tree, which is what happens running pytest from `contract/`. CI runs it from the repo root against an installed package, which is the environment the claim is about. --- contract/build/lib/mfc/__init__.py | 1 - contract/build/lib/mfc/cli.py | 205 ----- contract/build/lib/mfc/lint.py | 119 --- .../lib/mfc/schema/build-1.0.schema.json | 192 ---- .../lib/mfc/schema/bundle-1.0.schema.json | 150 --- .../mfc/schema/declarations-1.0.schema.json | 261 ------ .../lib/mfc/schema/emission-1.0.schema.json | 309 ------- .../mfc/schema/environment-1.0.schema.json | 194 ---- .../lib/mfc/schema/resolution-1.0.schema.json | 239 ----- .../lib/mfc/schema/review-1.0.schema.json | 171 ---- contract/build/lib/mfc/validate.py | 102 --- contract/mfc.egg-info/PKG-INFO | 857 +++++++++++++++++- contract/mfc.egg-info/SOURCES.txt | 75 +- contract/tests/test_lint_schemas.py | 50 + 14 files changed, 977 insertions(+), 1948 deletions(-) delete mode 100644 contract/build/lib/mfc/__init__.py delete mode 100644 contract/build/lib/mfc/cli.py delete mode 100644 contract/build/lib/mfc/lint.py delete mode 100644 contract/build/lib/mfc/schema/build-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/bundle-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/declarations-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/emission-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/environment-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/resolution-1.0.schema.json delete mode 100644 contract/build/lib/mfc/schema/review-1.0.schema.json delete mode 100644 contract/build/lib/mfc/validate.py diff --git a/contract/build/lib/mfc/__init__.py b/contract/build/lib/mfc/__init__.py deleted file mode 100644 index 4a0dfd6..0000000 --- a/contract/build/lib/mfc/__init__.py +++ /dev/null @@ -1 +0,0 @@ -"""Tooling for the math-formalization contract.""" diff --git a/contract/build/lib/mfc/cli.py b/contract/build/lib/mfc/cli.py deleted file mode 100644 index 256aa9d..0000000 --- a/contract/build/lib/mfc/cli.py +++ /dev/null @@ -1,205 +0,0 @@ -"""The `mfc` command line. - -Subcommands land as the contract does. Today: `lint-schemas`. - -Exit codes are the contract with CI and are fixed: - -* ``0`` — clean -* ``1`` — findings (the check ran and something failed) -* ``2`` — usage or environment error (the check did not run) - -The distinction between 1 and 2 is load-bearing. A CI job that treats "the -linter crashed" as "the linter passed" is the vacuous pass this whole project -exists to make impossible. -""" - -from __future__ import annotations - -import argparse -import json -import sys -from pathlib import Path - -from .lint import FORBIDDEN_PROPERTY_NAMES, lint_schema -from .validate import ( - LoadError, - SCHEMA_DIR, - load_artifact, - schema_path_for, - validate_artifact, -) - -EXIT_OK = 0 -EXIT_FINDINGS = 1 -EXIT_USAGE = 2 - -#: Schemas are found here when `--schema-dir` is not given. They live inside -#: the package so an installed `mfc` can find them, which is what ADR-0009's -#: "mfc is a shared tool again" requires. -DEFAULT_SCHEMA_DIR = SCHEMA_DIR - - -def _load(path: Path) -> tuple[dict | None, str | None]: - try: - return json.loads(path.read_text(encoding="utf-8")), None - except json.JSONDecodeError as exc: - return None, f"invalid JSON: {exc}" - except OSError as exc: - return None, f"unreadable: {exc}" - - -def cmd_lint_schemas(args: argparse.Namespace) -> int: - schema_dir = Path(args.schema_dir) if args.schema_dir else DEFAULT_SCHEMA_DIR - if not schema_dir.is_dir(): - print(f"error: no such schema directory: {schema_dir}", file=sys.stderr) - return EXIT_USAGE - - paths = sorted(schema_dir.glob("*.schema.json")) - if not paths: - # An empty sweep is not a pass. A mis-pointed --schema-dir must not - # look identical to a clean run. - print(f"error: no *.schema.json files in {schema_dir}", file=sys.stderr) - return EXIT_USAGE - - findings = 0 - unreadable = 0 - for path in paths: - document, problem = _load(path) - if problem is not None: - print(f"error: {path.name}: {problem}", file=sys.stderr) - unreadable += 1 - continue - for finding in lint_schema(document): - print(f"{path.name}: {finding}", file=sys.stderr) - findings += 1 - - if unreadable: - return EXIT_USAGE - if findings: - print( - f"error: {findings} forbidden property name(s) across " - f"{len(paths)} schema(s). arXMCP CLAUDE.md 4.9 forbids any single " - f"token that collapses distinct trust questions; the banned set is " - f"{sorted(FORBIDDEN_PROPERTY_NAMES)}.", - file=sys.stderr, - ) - return EXIT_FINDINGS - - print(f"ok: {len(paths)} schema(s), no forbidden property names") - return EXIT_OK - - -def cmd_validate(args: argparse.Namespace) -> int: - path = Path(args.artifact) - if not path.is_file(): - print(f"error: no such artifact: {path}", file=sys.stderr) - return EXIT_USAGE - - try: - document = load_artifact(path) - except LoadError as exc: - print(f"error: {path.name}: {exc}", file=sys.stderr) - return EXIT_USAGE - except OSError as exc: - print(f"error: {path.name}: unreadable: {exc}", file=sys.stderr) - return EXIT_USAGE - - if args.schema: - schema_path = Path(args.schema) - declared = None - else: - if not isinstance(document, dict) or "schema_version" not in document: - print( - f"error: {path.name}: no top-level schema_version, so the schema " - f"cannot be inferred. Every contract artifact carries one; pass " - f"--schema only to debug.", - file=sys.stderr, - ) - return EXIT_USAGE - declared = document["schema_version"] - if not isinstance(declared, str): - print(f"error: {path.name}: schema_version is not a string", file=sys.stderr) - return EXIT_USAGE - try: - schema_path = schema_path_for(declared) - except LoadError as exc: - print(f"error: {path.name}: {exc}", file=sys.stderr) - return EXIT_USAGE - - if not schema_path.is_file(): - # A version this build does not carry is a HARD failure. There is no - # tolerant mode: silently skipping would let an artifact from a future - # contract version pass unchecked. - which = f"declared schema_version {declared!r}" if declared else str(schema_path) - print( - f"error: {path.name}: unsupported contract version -- {which} maps to " - f"{schema_path.name}, which this build does not carry.", - file=sys.stderr, - ) - return EXIT_USAGE - - schema_doc, problem = _load(schema_path) - if problem is not None: - print(f"error: {schema_path.name}: {problem}", file=sys.stderr) - return EXIT_USAGE - - try: - problems = validate_artifact(document, schema_doc) - except LoadError as exc: - # The check did not run. Exit 2, never 1 -- see validate_artifact. - print(f"error: {exc}", file=sys.stderr) - return EXIT_USAGE - - if problems: - for p in problems: - print(f"{path.name}: {p}", file=sys.stderr) - print( - f"error: {path.name}: {len(problems)} problem(s) against {schema_path.name}", - file=sys.stderr, - ) - return EXIT_FINDINGS - - print(f"ok: {path.name} validates against {schema_path.name}") - return EXIT_OK - - -def build_parser() -> argparse.ArgumentParser: - parser = argparse.ArgumentParser( - prog="mfc", - description="Tooling for the math-formalization contract.", - ) - sub = parser.add_subparsers(dest="command", required=True) - - lint = sub.add_parser( - "lint-schemas", - help="reject schemas declaring a forbidden property name", - ) - lint.add_argument( - "--schema-dir", - help=f"directory of *.schema.json (default: {DEFAULT_SCHEMA_DIR})", - ) - lint.set_defaults(func=cmd_lint_schemas) - - val = sub.add_parser( - "validate", - help="validate an artifact against the schema it declares", - ) - val.add_argument("artifact", help="path to a .json or .yaml contract artifact") - val.add_argument( - "--schema", - help="override the schema path (debugging only -- the schema is " - "normally inferred from the artifact's own schema_version)", - ) - val.set_defaults(func=cmd_validate) - - return parser - - -def main(argv: list[str] | None = None) -> int: - parser = build_parser() - args = parser.parse_args(argv) - return args.func(args) - - -if __name__ == "__main__": # pragma: no cover - raise SystemExit(main()) diff --git a/contract/build/lib/mfc/lint.py b/contract/build/lib/mfc/lint.py deleted file mode 100644 index 844708a..0000000 --- a/contract/build/lib/mfc/lint.py +++ /dev/null @@ -1,119 +0,0 @@ -"""`mfc lint-schemas` — the banned-property lint. - -arXMCP's `CLAUDE.md` §4.9 forbids any single token that collapses distinct -trust questions into one. A schema that declares a property named `status` or -`verified` hands a producer that token back. This module is what turns that -policy from a review habit into a machine constraint: a schema declaring a -banned name fails, in CI, without anyone having to notice. - -## The traversal is deep, and that is not gold-plating - -The design note specifies this check as "walking every `properties` key of -every schema in `schema/`". That is the shallow reading, and it is inadequate -against the very first schema it would be run on: `emission/1.0` puts -`constant` and `cite` in `$defs`, so a top-level `doc["properties"]` walk never -sees `relation_claimed`, `axioms`, `type_pp`, or any of the other names that -actually matter. - -A banned name can be declared under any of: - - properties, patternProperties, $defs, definitions, - allOf/anyOf/oneOf branches, items, prefixItems, contains, - additionalProperties/unevaluatedProperties when they are schemas, - if/then/else, not, dependentSchemas, propertyNames - -so the walk recurses through all of them. `$ref` is deliberately NOT followed — -a `$ref` points at a definition this walk already visits directly, and -following it would double-report and can cycle. - -## Why 13 names and not 6 - -The design note's literal `FORBIDDEN_PROPERTY_NAMES` is 13 names; GitHub -issues #19 and #21 quote 6. The 13-name set is a strict superset and is the -literal artifact the design specifies, so it is what is implemented. The -discrepancy is recorded here rather than silently resolved, because this list -*is* the rule being mechanised — if the shorter list was intended, this is the -one place that has to change. -""" - -from __future__ import annotations - -from typing import Any, Iterator, NamedTuple - -#: Property names a contract schema may never declare. See the module docstring -#: for why this is the 13-name set rather than the 6-name one. -FORBIDDEN_PROPERTY_NAMES = frozenset({ - "status", "verified", "ok", "passed", "pass", "trusted", "result", - "verdict", "score", "confidence", "valid", "success", "clean", -}) - -#: Keywords whose value is a *map of name to schema*. The keys are declared -#: property names and are what the lint judges. -_PROPERTY_MAPS = ("properties", "patternProperties", "dependentSchemas") - -#: Keywords whose value is a *map of name to schema*, where the keys are -#: definition names rather than property names — recursed into, not judged. -_SCHEMA_MAPS = ("$defs", "definitions") - -#: Keywords whose value is a *list of schemas*. -_SCHEMA_LISTS = ("allOf", "anyOf", "oneOf", "prefixItems") - -#: Keywords whose value is a *single schema*. -_SCHEMA_VALUES = ( - "items", "contains", "not", "if", "then", "else", - "additionalProperties", "unevaluatedProperties", "propertyNames", - "additionalItems", "unevaluatedItems", -) - - -class Finding(NamedTuple): - """One banned property name, and where it was declared.""" - - path: str - """JSON-pointer-ish location, e.g. `$defs.cite.properties.status`.""" - name: str - """The offending property name.""" - - def __str__(self) -> str: # pragma: no cover - trivial - return f"{self.path}: declares forbidden property name {self.name!r}" - - -def _walk(node: Any, path: str) -> Iterator[Finding]: - """Yield a Finding for every banned property name declared under `node`.""" - if isinstance(node, list): - for i, item in enumerate(node): - yield from _walk(item, f"{path}[{i}]") - return - if not isinstance(node, dict): - return - - for keyword in _PROPERTY_MAPS: - block = node.get(keyword) - if isinstance(block, dict): - for name, subschema in block.items(): - if name in FORBIDDEN_PROPERTY_NAMES: - yield Finding(f"{path}{keyword}.{name}", name) - yield from _walk(subschema, f"{path}{keyword}.{name}.") - - for keyword in _SCHEMA_MAPS: - block = node.get(keyword) - if isinstance(block, dict): - for name, subschema in block.items(): - yield from _walk(subschema, f"{path}{keyword}.{name}.") - - for keyword in _SCHEMA_LISTS: - block = node.get(keyword) - if isinstance(block, list): - for i, subschema in enumerate(block): - yield from _walk(subschema, f"{path}{keyword}[{i}].") - - for keyword in _SCHEMA_VALUES: - subschema = node.get(keyword) - # `additionalProperties: false` is a boolean, not a schema; skip it. - if isinstance(subschema, (dict, list)): - yield from _walk(subschema, f"{path}{keyword}.") - - -def lint_schema(document: Any) -> list[Finding]: - """Every banned property name declared anywhere in `document`.""" - return list(_walk(document, "")) diff --git a/contract/build/lib/mfc/schema/build-1.0.schema.json b/contract/build/lib/mfc/schema/build-1.0.schema.json deleted file mode 100644 index 666a939..0000000 --- a/contract/build/lib/mfc/schema/build-1.0.schema.json +++ /dev/null @@ -1,192 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/build-1.0.schema.json", - "title": "build/1.0 - what the build actually reported", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "env_digest", - "lake_build_exit", - "lake_build_jobs", - "diagnostics", - "error_count", - "warning_count", - "sorry_diagnostic_count", - "independent_checkers", - "ci", - "produced_at" - ], - "properties": { - "schema_version": { - "const": "build/1.0" - }, - "env_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "lake_build_exit": { - "type": "integer", - "$comment": "RECORDED, NEVER THE GATE. Measured on this toolchain: `lake env lean` on a file whose #print axioms prints [sorryAx] exits 0, and so does -E hasSorry. sorry_diagnostic_count is the gate." - }, - "lake_build_jobs": { - "type": "integer", - "minimum": 0 - }, - "diagnostics": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "file_name", - "severity", - "kind", - "pos", - "end_pos", - "data" - ], - "properties": { - "file_name": { - "type": "string" - }, - "severity": { - "type": "string" - }, - "kind": { - "type": "string" - }, - "pos": { - "type": "object", - "additionalProperties": false, - "required": [ - "line", - "column" - ], - "properties": { - "line": { - "type": "integer" - }, - "column": { - "type": "integer" - } - } - }, - "end_pos": { - "type": "object", - "additionalProperties": false, - "required": [ - "line", - "column" - ], - "properties": { - "line": { - "type": "integer" - }, - "column": { - "type": "integer" - } - } - }, - "data": { - "type": "string" - } - } - } - }, - "error_count": { - "type": "integer", - "minimum": 0 - }, - "warning_count": { - "type": "integer", - "minimum": 0 - }, - "sorry_diagnostic_count": { - "type": "integer", - "minimum": 0, - "$comment": "Counted from NDJSON records with kind == hasSorry, never from the exit code." - }, - "independent_checkers": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "version", - "value", - "allow_sorry" - ], - "properties": { - "name": { - "type": "string" - }, - "version": { - "type": "string" - }, - "value": { - "enum": [ - "pass", - "fail", - "not_run", - "not_applicable" - ] - }, - "allow_sorry": { - "type": "boolean" - } - }, - "allOf": [ - { - "$comment": "A checker that passed WHILE PERMITTING sorry has not checked the thing this axis is about.", - "if": { - "properties": { - "value": { - "const": "pass" - } - }, - "required": [ - "value" - ] - }, - "then": { - "properties": { - "allow_sorry": { - "const": false - } - } - } - } - ] - } - }, - "ci": { - "type": "object", - "additionalProperties": false, - "required": [ - "run_url", - "workflow_sha", - "runner" - ], - "properties": { - "run_url": { - "type": [ - "string", - "null" - ] - }, - "workflow_sha": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "runner": { - "type": "string" - } - } - }, - "produced_at": { - "type": "string" - } - } -} diff --git a/contract/build/lib/mfc/schema/bundle-1.0.schema.json b/contract/build/lib/mfc/schema/bundle-1.0.schema.json deleted file mode 100644 index a4094c3..0000000 --- a/contract/build/lib/mfc/schema/bundle-1.0.schema.json +++ /dev/null @@ -1,150 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/bundle-1.0.schema.json", - "title": "bundle/1.0 - in-toto Statement v1, with no aggregate verdict", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "_type", - "subject", - "contract_repo", - "env_digest", - "registry_sha256", - "predicates", - "unrecognized_predicates" - ], - "properties": { - "schema_version": { - "const": "bundle/1.0" - }, - "_type": { - "const": "https://in-toto.io/Statement/v1" - }, - "subject": { - "type": "array", - "minItems": 1, - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "uri", - "digest" - ], - "properties": { - "name": { - "type": "string" - }, - "uri": { - "type": "string" - }, - "digest": { - "type": "object", - "additionalProperties": false, - "required": [ - "gitCommit" - ], - "properties": { - "gitCommit": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "gitTag": { - "type": [ - "string", - "null" - ] - } - } - } - } - } - }, - "contract_repo": { - "type": "object", - "additionalProperties": false, - "required": [ - "url", - "rev" - ], - "properties": { - "url": { - "type": "string" - }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - } - } - }, - "env_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "registry_sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "predicates": { - "type": "array", - "items": { - "$ref": "#/$defs/predicate" - } - }, - "unrecognized_predicates": { - "type": "array", - "items": { - "$ref": "#/$defs/predicate" - }, - "$comment": "Unknown predicateTypes are INGESTED, NEVER SERVED. formal_release_pin.py moves any type absent from the vendored predicate-types.json here and records it. That is what makes the URI extension point safe." - } - }, - "$defs": { - "predicate": { - "type": "object", - "additionalProperties": false, - "required": [ - "predicateType", - "file", - "sha256", - "produced_by", - "produced_at", - "env_digest", - "self_attested" - ], - "properties": { - "predicateType": { - "type": "string", - "format": "uri" - }, - "file": { - "type": "string", - "minLength": 1 - }, - "sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "produced_by": { - "type": "string" - }, - "produced_at": { - "type": "string" - }, - "env_digest": { - "type": [ - "string", - "null" - ], - "pattern": "^[0-9a-f]{64}$" - }, - "self_attested": { - "type": "boolean", - "$comment": "REQUIRED. Honest labelling for a solo-operated repo: true means the party that wrote the code also produced this measurement." - } - } - } - }, - "$comment": "SLSA's VerificationSummaryAttestation is DELIBERATELY NOT USED. Its verificationResult: PASSED|FAILED is exactly the single collapsed trust token arXMCP CLAUDE.md 4.9 forbids. One subject, N independently-dated, independently-sourced predicates, no aggregate." -} diff --git a/contract/build/lib/mfc/schema/declarations-1.0.schema.json b/contract/build/lib/mfc/schema/declarations-1.0.schema.json deleted file mode 100644 index 62b4141..0000000 --- a/contract/build/lib/mfc/schema/declarations-1.0.schema.json +++ /dev/null @@ -1,261 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/declarations-1.0.schema.json", - "title": "declarations/1.0 - recomputed from the emission", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "env_digest", - "emission_sha256", - "statement_digest_version", - "counts", - "declarations" - ], - "properties": { - "schema_version": { - "const": "declarations/1.0" - }, - "env_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "emission_sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "statement_digest_version": { - "type": "string", - "minLength": 1 - }, - "counts": { - "type": "object", - "additionalProperties": false, - "required": [ - "total", - "in_scope", - "internal", - "cited" - ], - "properties": { - "total": { - "type": "integer", - "minimum": 0 - }, - "in_scope": { - "type": "integer", - "minimum": 0 - }, - "internal": { - "type": "integer", - "minimum": 0 - }, - "cited": { - "type": "integer", - "minimum": 0 - } - } - }, - "declarations": { - "type": "array", - "items": { - "$ref": "#/$defs/declaration" - } - } - }, - "$defs": { - "declaration": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "module", - "kind", - "is_internal", - "statement_digest", - "local_deps", - "axioms", - "axioms_disallowed", - "contains_sorry_ax", - "local_axioms", - "range", - "cites" - ], - "properties": { - "name": { - "type": "string", - "minLength": 1 - }, - "module": { - "type": "string", - "minLength": 1 - }, - "kind": { - "enum": [ - "axiom", - "def", - "theorem", - "opaque", - "quot", - "inductive", - "ctor", - "rec" - ] - }, - "is_internal": { - "type": "boolean" - }, - "statement_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "local_deps": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "axioms": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "axioms_disallowed": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true, - "$comment": "RECOMPUTED by mfc against axiom_policy. The emission never reports this field." - }, - "contains_sorry_ax": { - "type": "boolean" - }, - "local_axioms": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "range": { - "oneOf": [ - { - "type": "null" - }, - { - "type": "object", - "additionalProperties": false, - "required": [ - "startLine", - "startCol", - "endLine", - "endCol" - ], - "properties": { - "startLine": { - "type": "integer" - }, - "startCol": { - "type": "integer" - }, - "endLine": { - "type": "integer" - }, - "endCol": { - "type": "integer" - } - } - } - ] - }, - "cites": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "key", - "relation_claimed", - "frontier", - "note" - ], - "properties": { - "key": { - "type": "string", - "pattern": "^stmt:[0-9a-f]{12}:[a-z][a-z0-9._-]{0,63}$" - }, - "relation_claimed": { - "enum": [ - "exact", - "equivalent", - "specialization", - "one_way", - "no_claim" - ] - }, - "frontier": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "note": { - "type": [ - "string", - "null" - ] - } - } - } - } - }, - "allOf": [ - { - "$comment": "A declaration carrying sorryAx must report it in BOTH places, consistently. The invalid/sorry-laundered fixture flips exactly one and MUST be rejected.", - "if": { - "properties": { - "contains_sorry_ax": { - "const": true - } - }, - "required": [ - "contains_sorry_ax" - ] - }, - "then": { - "properties": { - "axioms": { - "contains": { - "const": "sorryAx" - } - } - } - } - }, - { - "if": { - "properties": { - "axioms": { - "contains": { - "const": "sorryAx" - } - } - } - }, - "then": { - "properties": { - "contains_sorry_ax": { - "const": true - } - } - } - } - ] - } - } -} diff --git a/contract/build/lib/mfc/schema/emission-1.0.schema.json b/contract/build/lib/mfc/schema/emission-1.0.schema.json deleted file mode 100644 index b5a2df1..0000000 --- a/contract/build/lib/mfc/schema/emission-1.0.schema.json +++ /dev/null @@ -1,309 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/emission-1.0.schema.json", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "emitter_version", - "lean_version", - "lean_githash", - "lean_options", - "pp_options", - "root_lib", - "modules", - "counts", - "constants", - "emitted_at" - ], - "properties": { - "schema_version": { - "const": "emission/1.0" - }, - "emitter_version": { - "type": "string", - "pattern": "^mfc-emit/[0-9]+\\.[0-9]+\\.[0-9]+$" - }, - "lean_version": { - "type": "string" - }, - "lean_githash": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "lean_options": { - "type": "object", - "additionalProperties": { - "type": [ - "boolean", - "integer", - "string" - ] - } - }, - "pp_options": { - "type": "object", - "additionalProperties": { - "type": [ - "boolean", - "integer", - "string" - ] - } - }, - "root_lib": { - "type": "string" - }, - "modules": { - "type": "array", - "minItems": 1, - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "counts": { - "type": "object", - "additionalProperties": false, - "required": [ - "total", - "in_scope", - "internal", - "with_range", - "instances", - "private" - ], - "properties": { - "total": { - "type": "integer", - "minimum": 1 - }, - "in_scope": { - "type": "integer", - "minimum": 1 - }, - "internal": { - "type": "integer", - "minimum": 0 - }, - "with_range": { - "type": "integer", - "minimum": 0 - }, - "instances": { - "type": "integer", - "minimum": 0 - }, - "private": { - "type": "integer", - "minimum": 0 - } - }, - "$comment": "minimum:1 on total and in_scope is the VACUOUS-PASS GUARD. An emission of zero constants is the observable signature of a mis-scoped emitter, and it must not validate." - }, - "constants": { - "type": "array", - "minItems": 1, - "items": { - "$ref": "#/$defs/constant" - } - }, - "emitted_at": { - "type": "string" - } - }, - "$defs": { - "constant": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "module", - "kind", - "is_instance", - "is_internal", - "is_private", - "is_reducible", - "num_levels", - "type_pp", - "value_pp", - "local_deps", - "scc_members", - "axioms", - "range", - "cites" - ], - "properties": { - "name": { - "type": "string", - "minLength": 1 - }, - "module": { - "type": "string", - "minLength": 1 - }, - "kind": { - "enum": [ - "axiom", - "def", - "theorem", - "opaque", - "quot", - "inductive", - "ctor", - "rec" - ] - }, - "is_instance": { - "type": "boolean" - }, - "is_internal": { - "type": "boolean" - }, - "is_private": { - "type": "boolean" - }, - "is_reducible": { - "type": "boolean" - }, - "num_levels": { - "type": "integer", - "minimum": 0 - }, - "type_pp": { - "type": "string", - "minLength": 1 - }, - "value_pp": { - "type": [ - "string", - "null" - ] - }, - "local_deps": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true, - "$comment": "SORTED. Topic-local constants only." - }, - "scc_members": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "axioms": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true, - "$comment": "FULL transitive closure from Lean.collectAxioms, SORTED. collectAxioms returns them UNSORTED -- measured: [propext, Quot.sound, Classical.choice] on one decl and [Quot.sound, propext, Classical.choice] on the next in the same run. Sorting is REQUIRED for byte-reproducibility." - }, - "range": { - "oneOf": [ - { - "type": "null" - }, - { - "type": "object", - "additionalProperties": false, - "required": [ - "startLine", - "startCol", - "endLine", - "endCol" - ], - "properties": { - "startLine": { - "type": "integer" - }, - "startCol": { - "type": "integer" - }, - "endLine": { - "type": "integer" - }, - "endCol": { - "type": "integer" - } - } - } - ] - }, - "cites": { - "type": "array", - "items": { - "$ref": "#/$defs/cite" - } - } - }, - "allOf": [ - { - "$comment": "value_pp is statement-relevant ONLY for these kinds; anywhere else it would fold a PROOF TERM into a statement digest, making every proof edit look like a statement change.", - "if": { - "not": { - "properties": { - "kind": { - "enum": [ - "def", - "opaque" - ] - } - } - } - }, - "then": { - "properties": { - "value_pp": { - "type": "null" - } - } - } - } - ] - }, - "cite": { - "type": "object", - "additionalProperties": false, - "required": [ - "key", - "relation_claimed", - "frontier", - "note" - ], - "properties": { - "key": { - "type": "string", - "pattern": "^stmt:[0-9a-f]{12}:[a-z][a-z0-9._-]{0,63}$" - }, - "relation_claimed": { - "enum": [ - "exact", - "equivalent", - "specialization", - "one_way", - "no_claim" - ], - "$comment": "ALWAYS spelled `relation_claimed` in machine artifacts. `relation_confirmed` exists ONLY inside review/1.0. An agent reading this field reads the word 'claimed'." - }, - "frontier": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "note": { - "type": [ - "string", - "null" - ] - } - } - } - } -} diff --git a/contract/build/lib/mfc/schema/environment-1.0.schema.json b/contract/build/lib/mfc/schema/environment-1.0.schema.json deleted file mode 100644 index 1a128ce..0000000 --- a/contract/build/lib/mfc/schema/environment-1.0.schema.json +++ /dev/null @@ -1,194 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/environment-1.0.schema.json", - "title": "environment/1.0 - the pinned Lean environment", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "env_digest", - "env_digest_algorithm", - "lean_toolchain", - "lean_githash", - "lean_options", - "lake_version", - "packages", - "input_rev_is_branch", - "root_package", - "axiom_policy", - "emitter_version", - "mfc_version", - "contract_repo" - ], - "properties": { - "schema_version": { - "const": "environment/1.0" - }, - "env_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "env_digest_algorithm": { - "type": "string", - "minLength": 1 - }, - "lean_toolchain": { - "type": "string", - "minLength": 1 - }, - "lean_githash": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "lean_options": { - "type": "object", - "additionalProperties": { - "type": [ - "boolean", - "integer", - "string" - ] - } - }, - "lake_version": { - "type": "string", - "minLength": 1 - }, - "packages": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "rev", - "url", - "input_rev", - "inherited" - ], - "properties": { - "name": { - "type": "string", - "minLength": 1 - }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "url": { - "type": "string" - }, - "input_rev": { - "type": "string" - }, - "inherited": { - "type": "boolean" - } - } - } - }, - "input_rev_is_branch": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true, - "$comment": "GENERATED, not authored: every package whose inputRev is not a 40-hex, i.e. every package a `lake update` would silently re-resolve. Emitted so the drift risk is visible in the trust record, and it is why env_digest hashes rev and never inputRev." - }, - "root_package": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "url", - "rev", - "tag", - "worktree_dirty" - ], - "properties": { - "name": { - "type": "string", - "minLength": 1 - }, - "url": { - "type": "string" - }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - }, - "tag": { - "type": [ - "string", - "null" - ], - "$comment": "A NULL TAG IS A VALID ARTIFACT BUT AN INVALID RELEASE - formal_release_pin.py refuses to pin it. This is the mechanical statement of 'arXMCP pins RELEASED formalizations'." - }, - "worktree_dirty": { - "type": "boolean", - "$comment": "true fails mfc lint in CI mode." - } - } - }, - "axiom_policy": { - "type": "object", - "additionalProperties": false, - "required": [ - "allowlist", - "additions" - ], - "properties": { - "allowlist": { - "type": "array", - "items": { - "type": "string" - }, - "uniqueItems": true - }, - "additions": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "axiom", - "reason" - ], - "properties": { - "axiom": { - "type": "string" - }, - "reason": { - "type": "string", - "minLength": 1 - } - } - } - } - } - }, - "emitter_version": { - "type": "string" - }, - "mfc_version": { - "type": "string" - }, - "contract_repo": { - "type": "object", - "additionalProperties": false, - "required": [ - "url", - "rev" - ], - "properties": { - "url": { - "type": "string" - }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - } - } - } - } -} diff --git a/contract/build/lib/mfc/schema/resolution-1.0.schema.json b/contract/build/lib/mfc/schema/resolution-1.0.schema.json deleted file mode 100644 index 1f45b56..0000000 --- a/contract/build/lib/mfc/schema/resolution-1.0.schema.json +++ /dev/null @@ -1,239 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/resolution-1.0.schema.json", - "title": "resolution/1.0 - the one artifact arXMCP produces", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "registry_sha256", - "notebook", - "corpus_version", - "corpus_manifest_content_hash", - "resolver_version", - "chunker_version", - "generated_at", - "results", - "counts" - ], - "properties": { - "schema_version": { - "const": "resolution/1.0" - }, - "registry_sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$", - "$comment": "THE ENTIRE CROSS-REPO FRESHNESS MECHANISM. One comparison, no clocks, no mtimes, no network. Editing the registry without re-running the resolver turns CI red, and there is no way to forget." - }, - "notebook": { - "type": "string", - "minLength": 1 - }, - "corpus_version": { - "type": "integer", - "minimum": 0 - }, - "corpus_manifest_content_hash": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "resolver_version": { - "type": "string" - }, - "chunker_version": { - "type": "string" - }, - "generated_at": { - "type": "string" - }, - "results": { - "type": "array", - "items": { - "$ref": "#/$defs/result" - } - }, - "counts": { - "type": "object", - "additionalProperties": false, - "required": [ - "current", - "drifted", - "unresolvable", - "paper_absent", - "not_run" - ], - "properties": { - "current": { - "type": "integer", - "minimum": 0 - }, - "drifted": { - "type": "integer", - "minimum": 0 - }, - "unresolvable": { - "type": "integer", - "minimum": 0 - }, - "paper_absent": { - "type": "integer", - "minimum": 0 - }, - "not_run": { - "type": "integer", - "minimum": 0 - } - } - } - }, - "$defs": { - "result": { - "type": "object", - "additionalProperties": false, - "required": [ - "key", - "resolution", - "matched_by", - "chunk_id", - "matched_body_sha256", - "printed_number", - "similarity", - "reason" - ], - "properties": { - "key": { - "type": "string", - "pattern": "^stmt:[0-9a-f]{12}:[a-z][a-z0-9._-]{0,63}$" - }, - "resolution": { - "enum": [ - "current", - "drifted", - "unresolvable", - "paper_absent", - "not_run" - ] - }, - "matched_by": { - "enum": [ - "quote_sha256", - "printed_number", - "fuzzy", - "none" - ] - }, - "chunk_id": { - "type": [ - "string", - "null" - ] - }, - "matched_body_sha256": { - "type": [ - "string", - "null" - ], - "pattern": "^[0-9a-f]{64}$" - }, - "printed_number": { - "type": [ - "string", - "null" - ] - }, - "similarity": { - "type": [ - "number", - "null" - ], - "minimum": 0, - "maximum": 1 - }, - "reason": { - "type": [ - "string", - "null" - ] - } - }, - "allOf": [ - { - "$comment": "`current` REQUIRES a recomputed body digest. A resolver that says current without showing its work is rejected.", - "if": { - "properties": { - "resolution": { - "const": "current" - } - }, - "required": [ - "resolution" - ] - }, - "then": { - "required": [ - "matched_body_sha256", - "chunk_id" - ], - "properties": { - "matched_body_sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "chunk_id": { - "type": "string" - } - } - } - }, - { - "$comment": "A FUZZY match can NEVER be current. Nearest-neighbour similarity is not identity - this is the single line that stops a dense-ANN retrieval system silently re-pointing a citation at a different theorem.", - "if": { - "properties": { - "matched_by": { - "const": "fuzzy" - } - }, - "required": [ - "matched_by" - ] - }, - "then": { - "properties": { - "resolution": { - "enum": [ - "drifted", - "unresolvable" - ] - }, - "similarity": { - "type": "number" - } - } - } - }, - { - "$comment": "printed_number is a HINT. It is populated only on the ar5iv/LaTeXML path (36 of 66 chunks even on the flagship paper), and authors renumber between versions.", - "if": { - "properties": { - "matched_by": { - "const": "printed_number" - } - }, - "required": [ - "matched_by" - ] - }, - "then": { - "properties": { - "resolution": { - "enum": [ - "drifted" - ] - } - } - } - } - ] - } - } -} diff --git a/contract/build/lib/mfc/schema/review-1.0.schema.json b/contract/build/lib/mfc/schema/review-1.0.schema.json deleted file mode 100644 index 95a3a5b..0000000 --- a/contract/build/lib/mfc/schema/review-1.0.schema.json +++ /dev/null @@ -1,171 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://github.com/chris-dare-dev/math-formal-contract-lean/schema/review-1.0.schema.json", - "title": "review/1.0 - the only contract file no machine may write", - "type": "object", - "additionalProperties": false, - "required": [ - "schema_version", - "reviews" - ], - "properties": { - "schema_version": { - "const": "review/1.0" - }, - "reviews": { - "type": "array", - "items": { - "$ref": "#/$defs/review" - } - } - }, - "$defs": { - "review": { - "type": "object", - "additionalProperties": false, - "required": [ - "key", - "decl", - "reviewer", - "reviewed_at", - "reviewed_statement_digest", - "reviewed_quote_sha256", - "reviewed_env_digest", - "faithfulness", - "relation_confirmed", - "divergences" - ], - "properties": { - "key": { - "type": "string", - "pattern": "^stmt:[0-9a-f]{12}:[a-z][a-z0-9._-]{0,63}$" - }, - "decl": { - "type": "string", - "minLength": 1 - }, - "reviewer": { - "type": "object", - "additionalProperties": false, - "required": [ - "name" - ], - "properties": { - "name": { - "type": "string", - "minLength": 1 - }, - "email": { - "type": [ - "string", - "null" - ] - }, - "affiliation": { - "type": [ - "string", - "null" - ] - } - } - }, - "reviewed_at": { - "type": "string", - "pattern": "^[0-9]{4}-[0-9]{2}-[0-9]{2}$" - }, - "reviewed_statement_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "reviewed_quote_sha256": { - "type": [ - "string", - "null" - ], - "pattern": "^[0-9a-f]{64}$" - }, - "reviewed_env_digest": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "faithfulness": { - "enum": [ - "adequate", - "divergent", - "inadequate", - "inconclusive" - ], - "$comment": "`inconclusive` is a COMPLETE and LEGITIMATE outcome - abstention is a success, not a failure. There is deliberately no agent_drafted state: it would let an LLM verdict occupy the one axis that exists to catch what an LLM cannot." - }, - "relation_confirmed": { - "enum": [ - "exact", - "equivalent", - "specialization", - "one_way", - "no_claim", - "disputed" - ], - "$comment": "relation_confirmed appears ONLY in this file. Machine artifacts always say relation_claimed." - }, - "divergences": { - "type": "array", - "items": { - "type": "string" - } - }, - "note": { - "type": [ - "string", - "null" - ] - } - }, - "allOf": [ - { - "$comment": "A divergent or inadequate verdict without a written divergence is not a review.", - "if": { - "properties": { - "faithfulness": { - "enum": [ - "divergent", - "inadequate" - ] - } - }, - "required": [ - "faithfulness" - ] - }, - "then": { - "properties": { - "divergences": { - "minItems": 1 - } - } - } - }, - { - "$comment": "`exact` confirmed with a stated divergence is self-contradictory.", - "if": { - "properties": { - "relation_confirmed": { - "const": "exact" - } - }, - "required": [ - "relation_confirmed" - ] - }, - "then": { - "properties": { - "divergences": { - "maxItems": 0 - } - } - } - } - ] - } - } -} diff --git a/contract/build/lib/mfc/validate.py b/contract/build/lib/mfc/validate.py deleted file mode 100644 index ad8dd79..0000000 --- a/contract/build/lib/mfc/validate.py +++ /dev/null @@ -1,102 +0,0 @@ -"""`mfc validate` — check an artifact against its schema. - -## The schema is inferred, not asked for - -Every contract artifact carries `schema_version` as its first key. `validate` -reads it and picks the schema from that, rather than taking a `--schema` flag. - -That is deliberate: it makes the artifact's **self-description** part of what -is checked. An artifact claiming `emission/1.0` is validated against -`emission/1.0` and cannot be quietly checked against something laxer, and an -artifact whose `schema_version` names a version this build does not carry is a -hard failure rather than a silent skip — which is the -`ContractVersionUnsupported` behaviour the design calls for. There is no -tolerant mode. - -`--schema` exists only to override for debugging, and saying so is the point: -if you have to pass it, something is already wrong. - -## All errors, not the first - -`jsonschema`'s `iter_errors` is used rather than `validate`. A validator that -stops at the first problem turns fixing a bad artifact into N round trips, and -for a cross-field `allOf` the first error is often the least informative one. -""" - -from __future__ import annotations - -import json -from pathlib import Path -from typing import Any, NamedTuple - -SCHEMA_DIR = Path(__file__).resolve().parent / "schema" - - -class LoadError(Exception): - """The artifact could not be read or parsed. Distinct from being invalid.""" - - -def schema_path_for(version: str) -> Path: - """`emission/1.0` -> `schema/emission-1.0.schema.json`.""" - if "/" not in version: - raise LoadError(f"schema_version {version!r} is not of the form /") - name, _, ver = version.partition("/") - return SCHEMA_DIR / f"{name}-{ver}.schema.json" - - -def load_artifact(path: Path) -> Any: - """Parse a JSON or YAML artifact. - - `attest/review.yaml` is genuinely YAML, so YAML is supported when PyYAML is - installed. When it is not, that is reported as a missing capability rather - than as an invalid artifact — the two are different facts and a caller - must be able to tell them apart. - """ - text = path.read_text(encoding="utf-8") - if path.suffix.lower() in {".yaml", ".yml"}: - try: - import yaml # noqa: PLC0415 - optional dependency, imported on demand - except ImportError as exc: # pragma: no cover - depends on environment - raise LoadError( - f"{path.name} is YAML but PyYAML is not installed; " - f"install the 'yaml' extra (pip install 'mfc[yaml]')" - ) from exc - try: - return yaml.safe_load(text) - except yaml.YAMLError as exc: - raise LoadError(f"invalid YAML: {exc}") from exc - try: - return json.loads(text) - except json.JSONDecodeError as exc: - raise LoadError(f"invalid JSON: {exc}") from exc - - -class Problem(NamedTuple): - location: str - message: str - - def __str__(self) -> str: # pragma: no cover - trivial - return f"{self.location}: {self.message}" - - -def validate_artifact(document: Any, schema: dict) -> list[Problem]: - """Every way `document` fails `schema`, not just the first. - - A missing `jsonschema` raises `LoadError`, never propagates. An unhandled - ImportError exits 1, and 1 means "this artifact is invalid" -- so a missing - dependency would be reported as a bad artifact. "I could not check this" - and "this is wrong" are different facts and must not share an exit code. - """ - try: - import jsonschema # noqa: PLC0415 - keeps `mfc lint-schemas` import-light - except ImportError as exc: # pragma: no cover - depends on environment - raise LoadError( - "jsonschema is not installed, so nothing was validated. " - "Install it (pip install mfc) -- this is NOT a statement about the artifact." - ) from exc - - validator = jsonschema.Draft202012Validator(schema) - return [ - Problem(error.json_path, error.message) - for error in sorted(validator.iter_errors(document), key=lambda e: list(e.path)) - ] diff --git a/contract/mfc.egg-info/PKG-INFO b/contract/mfc.egg-info/PKG-INFO index 9848c3e..52821bc 100644 --- a/contract/mfc.egg-info/PKG-INFO +++ b/contract/mfc.egg-info/PKG-INFO @@ -5,7 +5,7 @@ Summary: Schemas and tooling for the math-formalization contract Author: Chris Dare License: MIT Keywords: lean,formalization,provenance,json-schema -Requires-Python: >=3.9 +Requires-Python: >=3.11 Description-Content-Type: text/markdown Requires-Dist: jsonschema>=4.18 Provides-Extra: yaml @@ -38,14 +38,30 @@ to serve this directory, the named exception in the consuming repo's | path | what | |---|---| -| `mfc/schema/*.schema.json` | **all seven** artifact formats | -| `mfc/lint.py` | the banned-property lint | +| `mfc/schema/*.schema.json` | **all twelve** artifact formats | +| `mfc/digest.py` | the four canonical digest functions — **frozen** | +| `mfc/lint.py` | the banned-property lint, and the volatile-property lint | | `mfc/validate.py` | artifact validation | -| `mfc/cli.py` | `mfc lint-schemas`, `mfc validate` | +| `mfc/bundle.py` | `declarations.json`, everything recomputed | +| `mfc/build.py` | `build/1.0` from lake's NDJSON — the sorry count comes from `kind`, never the exit code | +| `mfc/seal.py` | `bundle/1.0`, the in-toto Statement `conformance` reads | +| `mfc/rules.py` | the E-01..E-10 content rules | +| `mfc/bootstrap.py` | the write-once `bootstrap` flag — how a repo with nothing in it yet reaches a first green build | +| `mfc/conformance.py` | the C-01..C-12 cross-artifact rules | +| `mfc/join.py` | the J-01..J-06 rules and the claim table | +| `mfc/ilean.py` | the I-01..I-05 coverage rules | +| `mfc/registry.py` | reading a `registry/1.0` document | +| `mfc/rules_registry.py` | the R-01..R-09 registry rules | +| `mfc/scaffold.py` | `mfc init` — the topic-repo templates | +| `mfc/env.py` | `mfc env` — reads a topic checkout, writes `environment/1.0` | +| `mfc/cli.py` | `mfc lint-schemas`, `validate`, `bundle`, `build`, `lint`, `conformance`, `seal`, `join`, `env`, `check-ilean-coverage`, `init`, `registry` | | `pyproject.toml` | packaging, so a consumer can install it | | `testdata/schemas/invalid/` | schemas that must fail the lint | | `testdata/artifacts/valid/` | one filled instance per schema | +| `testdata/emissions/bootstrap/` | the emission a repository has *before* it has any mathematics | | `testdata/artifacts/invalid/` | artifacts that must fail a cross-field rule | +| `testdata/registries/invalid/` | registries that must fail an `R` rule | +| `testdata/digests/` | the canonical **bytes** behind nine digests, hand-written and hashed with `shasum` | | `tests/` | pytest | ### How much of each schema was given, and how much was authored @@ -84,6 +100,62 @@ The last one is why `additionalProperties: false` is everywhere rather than just tidy: it is what stops a single collapsed trust token being added to an artifact at all. +### `run/1.0`: the artifact that exists in order not to be committed + +`git diff --exit-code attest/` is the only one of the four claimed sorry-gates +that survives the seam. Two separate things were wrong with it. + +**It could never pass.** `bundle.json` carried `produced_at` on every +predicate; `build.json` carried `produced_at` and `ci{run_url, workflow_sha, +runner}`. Both are committed, both changed on every run, so the gate went red +on no-op commits — and a gate that is red on no-op commits gets deleted within +the week, by someone who is right that it is broken and wrong about which half +to remove. + +**It could never fail either.** The generated `.gitignore` ignored +`/attest/*.json` wholesale, so the diff compared nothing at all. Fixing only +the first half would have produced a gate that passes for the wrong reason, +which is indistinguishable from the bug. + +Both are fixed. Everything that changes per run moved to `run/1.0` — +`attest/run.json`, gitignored, shipped as a release asset — and it names the +files it produced by `sha256`, so provenance still joins back to the committed +tree without anything in the committed tree moving. `contract_repo` stayed in +the bundle: `rev` is a **pin**, and a pin that changed every run would not be +pinning anything. + +`mfc lint-schemas` now fails on a `produced_at` in any of `declarations`, +`environment`, `bundle`, `build` — the four artifacts CI regenerates on every +commit and commits the result of. It does **not** police `review.reviewed_at` +or `resolution.generated_at`: those are committed, but they are written by a +deliberate human or offline act, and the date a person reviewed a statement is +the fact being recorded rather than run metadata. Banning them would delete +evidence to protect a gate they do not threaten. + +### Canonicalization is pinned by data, because there is only one implementation + +JSON-Schema-Test-Suite works because ~20 independent implementations run the +corpus. Here there is one, so "our code agrees with our code" proves nothing: a +canonicalization bug is symmetric and invisible to conformance. + +`testdata/digests/canonicalization.json` carries, for each of the nine cases, +the **exact bytes** fed to `sha256` — written by hand from the spec in +`digest.py` and hashed with `shasum(1)` — beside the digest of those bytes. +The tests then assert the datum is internally consistent using stdlib `hashlib` +alone, that `mfc` reproduces those bytes **byte for byte**, and that the +end-to-end digest matches. Under drift the first still passes and the second +fails, naming the bytes that moved. + +Three of the nine reproduce values the design note recorded as `[COMPUTED]` +against the real repository at `f166a3d`, months before this code existed — +hand-written canonical forms whose `shasum` matched numbers nobody could have +back-fitted. A fourth test set mutates the canonicalizer three plausible ways +(unsorted keys, default separators, `ensure_ascii=False`) and asserts each is +rejected, because assertions that cannot fail are the thing being fixed. + +The rule for adding a case is in `testdata/digests/README.md` and is one line: +never paste `mfc`'s own output. + ### One judgement call worth flagging The note's filled instances carry `$comment` keys as reader documentation. @@ -118,6 +190,783 @@ Two placement notes, both deliberate: Neither adds a Lake dependency, so the zero-dependency invariant is untouched. +## `lint`: a rule that did not run is not a rule that passed + +Schema validation says an artifact is well *formed*. The E-rules say whether +what it contains is *allowed* — a perfectly well-formed emission can still +launder a `sorry`, declare an undeclared axiom, or cite a key that does not +exist. + +Two rules cannot run yet. `E-04` needs the statement registry, which is gated +on the open size-ceiling decision, and `E-09` needs the topic's `closed_lanes` +configuration. They report **`not_run`**, never `pass`, and every invocation +prints which rules did not run instead of folding them into a count: + +``` +7 passed, 0 failed, 3 not_run +note: E-04, E-05, E-09 did NOT run. This is not a pass -- nothing checked + what they check. +``` + +That is the trust-axis rule applied one level down. A green lint with +`E-04: not_run` must not be readable as "the citations resolve". `--require-all` +turns any `not_run` into a failure, for the day the inputs exist. + +`E-05` shows the other half of the idea: its emission half (a citation claiming +`exact` while carrying its own open frontier) runs now and *fails* now; only +the registry half is deferred. A missing input suppresses exactly what it must +and no more. + +Every rule has a fixture in `testdata/emissions/invalid/` that must trip it. + +### The bootstrap flag, and why it burns down + +The vacuous-pass guard is structural: `emission-1.0.schema.json` sets +`constants: minItems 1` and `counts.total/in_scope: minimum 1`, so an empty +emission is not a representable artifact. That also made an adopter's **first** +build unreachable — a repository generated by `mfc init` has no declarations, +and the generated workflow emits before anything has been written. + +`formalization.yaml` carries `bootstrap: true`. While it is set, `validate`, +`bundle` and `lint` accept an empty emission against a copy of the schema with +exactly three constraints dropped (`bootstrap.RELAXED`, asserted by test to be +the only difference), and every E-rule reports **`not_run`** — a green table +over an empty emission would otherwise say "no declaration depends on +`sorryAx`" about a repository with no declarations. + +Three properties keep it from being an `--allow-empty` flag with a longer name: + +- **It burns down.** `mfc lint` clears it the first time it sees in-scope + declarations and stamps `bootstrap_cleared_at`. A record carrying that date + may never set `bootstrap: true` again — `bootstrap.read` raises on the + combination rather than honouring it. +- **It excuses one situation, not two.** An emission with constants and + `counts.in_scope: 0` is a *mis-scoped emitter*, and that is a defect on day + one exactly as it is on day one thousand. Bootstrap does not touch it. +- **A broken emission cannot burn it.** Clearing needs in-scope declarations, + not merely "not empty", so a bad emitter run cannot cost a repository its + bootstrap state permanently. + +The cleared record is left in the working tree for the operator to commit, +which is what `git diff --exit-code attest/`-style gates are for: clearing the +flag is a commit someone makes, not a fact CI invents. + +**`E-07` earns its keep twice.** It was written so two different statements +cannot hash identically. It also turns out to select exactly the statements +that cannot be re-elaborated — measured at 339/339 round-trip on elision-free +statements and 0/61 on elided ones — so it is already the precondition +`--restate-check` needs. + +## `env`: the record everything consumed and nothing produced + +`bundle` stamps `env_digest` onto declarations. `conformance` checks `C-05` and +`C-10` against it. `join` renders a review `not_applicable` when it disagrees. +All three read an `environment/1.0` record — and until now **nothing wrote one.** +In this repository's own CI the real emission is bundled against +`testdata/artifacts/valid/environment-1.0.json`, a *fixture*: the one artifact +meant to pin what the measurement was made in was describing a different machine. + +```bash +mfc env --repo ../topic-repo --out attest/environment.json \ + --axiom-allowlist propext,Quot.sound,Classical.choice \ + --emitter-version mfc-emit/1.0.0 +``` + +Every field is read out of the checkout — `lean-toolchain`, +`lake-manifest.json`, `lakefile.toml`, `git`. Two are inputs rather than +observations, and deliberately so: + +* **`axiom_policy`** is a policy, not a property of a build. Defaulting it would + be this package asserting a policy on a topic repo's behalf, so it is + required — the same reasoning that makes `@[cites]`'s `relation` mandatory. +* **`lean_githash` / `lake_version`** come from running the toolchain, and are + overridable so a caller without one on PATH supplies what it measured rather + than receiving a fabricated value. + +### What it says out loud + +Run against the consuming repo it reports, correctly and unprompted: + +``` + NOT PINNED 13 package(s) track a branch and would move on `lake update`: + Cli, LeanSearchClient, MD4Lean, Qq, aesop, batteries, importGraph, + informal, mathlib, plausible, proofwidgets, subverso, verso + UNTAGGED valid artifact, invalid release -- a release pin requires a tag +``` + +Thirteen of fifteen, **mathlib among them**. That is why `env_digest` hashes +`rev` and never `inputRev`: `inputRev` is what a caller asked for, `rev` is what +resolved, and hashing the ask would leave the digest stable across a real +environment change. `test_changing_input_rev_alone_does_not_move_the_digest` +pins that, with `test_changing_a_resolved_rev_does_move_the_digest` as its +control. + +A dirty worktree is **recorded, not refused** — refusing would make the tool +unusable mid-work, and dropping it would let a digest describe a tree that is +not in git. `mfc lint` is where dirty becomes fatal, in CI mode. + +A package with no resolved 40-hex `rev` is refused outright rather than +placeholdered: an unpinnable dependency inside a digest that claims to pin +everything is worse than no artifact. + +### It will not run against this package + +`mfc env --repo .` here fails with *"'MathFormalContract' is not in +lake-manifest.json"*, and that is correct. This is a leaf with no manifest +packages — it is the contract package, not a topic repo. Which also means this +repo's own CI cannot produce a real environment record for itself, and its use +of the fixture is a test of the emitter rather than a trust record. Read it that +way. + +## `build`: the exit code is not the measurement + +`lake env lean --json` on a file whose only defect is a `sorry` **exits 0**. +Measured on `leanprover/lean4:v4.32.1`, the pinned toolchain: + +``` +{"kind":"hasSorry","severity":"warning","data":"declaration uses `sorry`",...} +EXIT=0 +``` + +So `lake_build_exit` is recorded and never consulted, and the gate is +`sorry_diagnostic_count`, counted from records whose `kind` is `hasSorry`. This +is the emitter's "never parse the source" discipline one level down: in the +build log rather than in the declaration. + +Counting by `kind` has one silent failure mode — a toolchain that renames or +drops the tag turns every sorry into an uncounted warning and the count reads +`0`. A diagnostic whose *text* reads like a sorry while its `kind` says +otherwise is therefore a **hard failure**. The text is a tripwire and never the +counter: counting from prose would break the moment Lean rewords the message, +which is why the `kind` field exists at all. + +A line that is not a JSON object raises rather than being skipped. A diagnostic +that could not be parsed is a diagnostic that would not be counted, and an +undercount is indistinguishable from a clean build — so lake's human-readable +progress output on the same handle is reported as the caller error it is. + +`independent_checkers` is an input, not an observation, for the same reason +`axiom_policy` is: this package cannot know what else was run. An empty array +reads as "none was run", which is different from the field being absent. + +### `measured`: a clean build and an unmeasured build are the same document + +`error_count`, `warning_count` and `sorry_diagnostic_count` are all `0` whether +the build was spotless or the NDJSON covered one module of 494, and no other +field in `build/1.0` can tell those apart. That makes an unmeasured build the +most flattering artifact this package could write — the same absence +`check-ilean-coverage` exists for, one level down in the build log. + +It is not a hypothetical. Measured on `leanprover/lean4:v4.32.1`, there is no +cheap route to project-wide NDJSON: `lake env lean --json` on a root import +file prints **nothing**, because imports are served from oleans and never +re-reported; `moreLeanArgs = ["--json"]` is consumed by lake, which re-renders +messages in its own text format; lake persists no structured log under +`.lake/build`; and per-module invocation pays a full Mathlib import load each +time. A consumer repository's CI therefore measures a handful of modules, and +`measured` is what stops that reading as a clean sweep. + +Its numerator is **declared**, because a module that elaborated cleanly leaves +no trace in the log and cannot be recovered from it — `--covers MODULE`, or +`--covers-all` as a deliberate claim rather than a default. Its denominator is +**read from the emission's `modules[]`**, never from the caller, so the one +number that could be shrunk to flatter the other cannot be. A declared module +absent from that list is a hard failure: coverage may be narrow, and it may not +be invented. + +No ratio is stored. A reader divides two integers. A single `coverage: 100%` +would be the collapsed trust token every schema here refuses, and it would be +the first thing a tired reader believed. + +## `conformance`: seven valid artifacts that do not describe the same thing + +`validate` asks whether one artifact is well formed. `lint` asks whether one +emission contains anything forbidden. Neither can see the failure this command +exists for — a `build.json` measured before the last commit, a review performed +against an earlier environment, a `declarations.json` derived from an emission +other than the one shipped. Each file passes its own schema. The set is still a +lie. + +Twelve rules, all of them a link between two artifacts rather than a property of +one. `C-02` (a predicate's `sha256` is the file's actual bytes) is the load +bearer: without it every other link is between things the bundle merely +asserts. `C-07` is the only rule that checks a digest against the data it +summarizes rather than against another digest. + +### It writes no artifact, and that is the point + +The obvious shape is to emit `conformance.json` with a verdict in it. It +deliberately does not, because there is nowhere honest to put one — a +`conformance.json` carrying a top-level verdict *is* the `aggregate-verdict` +rejection fixture, mechanically produced by our own tool. + +Read that as "no aggregate verdicts", not "no files". `join --workqueue-out` +writes `workqueue/1.0` and does not breach this, because a work queue judges +nothing — see [`join`](#j-06-computes-the-queue-workqueue-out-writes-it-down). + +So the output is a report and an exit code, and the reviewable object is an +evidence table: + +``` +evidence + environment attest/environment.json mfc/1.0.0 self-attested this environment + human-review attest/review.json human:Chris Dare independent this environment + corpus-resolution attest/resolution.json arxmcp/statement_resolve.. independent n/a (not a Lean measurement) + provisional-self-reported attest/lean-verify-tran.. arxmcp/lean_verify@v4.31.0 self-attested OTHER environment (ffffffff...) + +6 predicate(s); 2 not self-attested; 1 produced in another environment +``` + +Three counts, printed separately and never combined, because "6 predicates" +must not be readable as "6 independent measurements of this build". No column +of that table is a score, and `test_no_row_carries_a_verdict` keeps it that way. + +### Out-of-environment evidence is labelled, not averaged in + +The reference bundle carries a transcript produced by a **v4.31.0** toolchain +against a repo pinned to **v4.29.0**. That is legitimate and must stay visibly +separate, which is what the `provisional-self-reported` predicate type is for. +`C-05` makes the label binding: a `build/v1` predicate carrying a foreign +`env_digest` is a measurement of another build presented as a measurement of +this one. + +There is one way to satisfy `C-05` without fixing anything — relabel the +predicate as provisional. That is the intended escape, not a hole: relabelling +*is* the retraction, and the table then shows a claim demoted to nothing. + +### Capturing `reviewed_statement_pp`, and why it proves itself + +`reviewed_statement_pp` is the string a review's survival depends on: +`restateOne` parses it, elaborates it, and asks `isDefEq` against the +declaration's current type. Every way of getting it wrong is **silent** — the +field looks captured, `mfc validate` passes, and the failure appears at the +next dependency bump as `not_checkable`, which reads like a broken tool rather +than a bad capture. + +Capturing the first real one by hand took three attempts: + +1. **Elision.** `pp.explicit` alone left a `⋯` inside a proof argument. + `pp.proofs`, `pp.deepTerms` and a raised `pp.maxSteps` close it — which is + why the capture builds on `Emit.ppOpts` rather than its own list. +2. **Invented universe names.** `#check @Decl` instantiates the constant with + fresh universe metavariables and prints them `u_1, u_2, u_3`; the + declaration's `levelParams` were `[w, u, u']`. `ci.type` carries the + declaration's own names, the term does not. +3. **A verification easier than the real check** — a `universe u_1 u_2 u_3` + command above an `example`, supplying by hand the level context + `restateOne` does not have. + +So `--capture` renders, then puts the result through `restateOne` itself — the +same parse, `elabTerm`, `isDefEq` and `withLevelNames` — and returns the string +**only** on `restated`. All three failures produce a rendering that fails that +check, so none can reach `review.yaml` through this path. A capture that cannot +pass the check it exists to feed is not a capture. + +### `C-10` and the bump that invalidates every review at once + +`env_digest` hashes every package rev, so a single dependency bump rotates it +while the mathematics sits still — and `C-10` then reports every human review +as belonging to another environment. This is not a hypothetical. It happened to +the **first review the consuming repository ever recorded**, hours after it was +written: `MathFormalContract` moved `d3df3818 → 21e3b442`, `env_digest` went +`45d9e8ca → 5b2b3d86`, and `C-10` failed while the reviewed statement's digest +was byte-identical on both sides. + +`C-10` was right to fail — the review *was* performed elsewhere — and the wrong +repair is to widen the rule or edit `reviewed_env_digest`, which is the one +thing a review must never suffer silently. + +So `conformance --restate` supplies evidence instead. A review whose +environment moved is carried forward when, and only when, the restate run says +`restated` for its key. `changed` is a finding: the statement moved and the +verdict describes something the declaration no longer says. A key the restate +run does not mention is a finding too, because an omitted entry reads exactly +like a checked one. + +`not_checkable` is a finding **worded as itself**. It is not reported as +`changed`, because the two send a reviewer to different places, and collapsing +them would hide a broken checker behind a pile of apparently-invalidated +reviews. Carried-forward reviews are counted in the rule's reason rather than +passing silently: a reader has to be able to tell a review performed here from +one inherited across a bump. + +### `C-12` and the vacuous pass, one level up + +Every other rule checks what is *present*. A bundle that simply omits its +`build/v1` predicate therefore satisfies all eleven and reports "5 +predicate(s)". `C-12` is the only rule that can see an absence, and +`test_c12_a_bundle_that_simply_omits_its_build_predicate` asserts that no other +rule notices — which is why it exists. + +### What used to be missing, and what still is + +This section previously read "nothing assembles a `bundle.json`, and there is +no `environment.json` or `build.json`, so there is nothing for `conformance` to +run against." Two of those three are now produced: `mfc env` writes the +environment record, and `mfc build` and `mfc seal` write the other two. The +consuming repository's CI produces `environment.json` and `declarations.json` +today, and `test_conformance_passes_over_a_sealed_bundle` runs all twelve rules +over a bundle this package actually wrote rather than one a test assembled. + +What is still absent is stated the same way rather than worked around. +`review.yaml` has no producer and must not have one — it is the axis no machine +may write. `resolution.json` is arXMCP's, and until it exists `C-08` and `C-10` +report `not_run`, which is **not** a pass: the summary line says so on every +run. + +### The fixture tree is built, not checked in + +`C-02` compares a predicate's `sha256` to real bytes, so a checked-in `attest/` +tree would need its digests hand-maintained on every edit. The cost of +generating it is that a generator and a checker sharing a misconception agree +with each other — which is what the mutation tests are for. Each takes the +coherent tree, breaks exactly one link, and requires the matching rule to +notice. + +Building that tree found a real defect in a checked-in fixture. `C-07` +recomputes the environment digest from the environment's own fields, and +`environment-1.0.json` declared a digest computed over **fourteen** packages +while listing **three** — the design note's instance, trimmed for readability, +with the real digest left in place. Rebuilt truthfully from the consuming +repo's `lake-manifest.json`, which also makes `digest.py`'s "nine of the +fourteen packages carry `inputRev` `main` or `master`" checkable against the +fixture instead of only asserted in prose. + +## `seal`: the producer `conformance` was waiting for + +Twelve rules, and until now nothing wrote the file they read. `mfc seal` +assembles `bundle/1.0` — an in-toto Statement v1 with one subject and N +predicates, and deliberately **no** SLSA `verificationResult`, which is exactly +the single collapsed trust token the design forbids. + +### It cannot write the `C-12` fixture + +`C-12` exists because every other rule checks what is *present*: a bundle that +omits its `build/v1` predicate satisfies all eleven others and reports "5 +predicate(s)". A producer willing to write that bundle would be shipping the +rejection fixture as a product, so `seal` refuses when a required predicate +type is missing — and there is no `--force`. The producer and the checker +import `REQUIRED_PREDICATE_TYPES` from the same module, so the two lists cannot +drift. + +### A dirty worktree is refused + +The subject attests a `gitCommit`. If the tree carries uncommitted changes, the +measurements describe bytes that commit does not contain, and every digest in +the bundle becomes a true statement about a tree nobody can fetch. +`--allow-dirty` exists for local experimentation and says on stderr that the +result is explicitly not a release. + +### `self_attested`, said rather than implied + +`true` means the party that wrote the code also produced the measurement. For a +solo-operated repository that is the honest label on `environment`, +`declarations` and `build`, and stating it is worth more than the appearance of +independence. Human review and the corpus resolution are produced elsewhere and +carry `false`. The corpus resolution also carries `env_digest: null` — not a +mismatch and not a match, because it is not produced in a Lean environment at +all. + +## `join`: three axes, three columns, no fourth column + +`conformance` asks whether the artifacts describe the same *build*. `join` asks +whether they describe the same *claims*. A review, a corpus resolution and a +citation each name a statement, and until now nothing checked that the three +ever meet. + +The output is the claim table — one row per `(registry key, declaration)` +binding: + +``` + key decl claimed faithful confirmed resolved frontier + stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2 Topic.thm one_way adequate one_way current - + stmt:9f4c1a20b7d3:bridgeland2007.prop-8.1 Topic.thm exact not_run not_run not_run gltilde-universal-cover +``` + +The second row is what the table exists for: the author claims `exact`, no +reviewer has looked, the corpus was never asked, and a frontier item is open. +No single token can say that, which is why there are separate columns and no +verdict — `test_no_column_is_a_verdict` keeps it that way. Absent evidence +prints `not_run`, so the table has no empty cells to misread. + +Run against this repo's own test emission it reports, correctly: + +``` +0 passed, 0 failed, 6 not_run +8 binding(s) over 8 key(s); 0 reviewed; 0 resolved; 1 with an open frontier +``` + +Nothing here is reviewed or resolved, and the output says so rather than +looking clean. + +### A verdict about another environment is not a weak verdict about this one + +The digest join answers *which statement was reviewed*. It says nothing about +*which environment the reviewer was looking at* — and a review of Lean v4.29 is +no evidence at all about a v4.31 build. That skew is not hypothetical: it is the +standing gap between this repo's pin and the one arXMCP's REPL runs. + +So `join` takes `--environment`, and a review whose `reviewed_env_digest` +disagrees with it renders `not_applicable`: + +``` + key decl claimed faithful confirmed resolved frontier + stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2 Topic.thm exact not_applicable not_applicable not_run - + +1 binding(s) over 1 key(s); 0 reviewed; 0 resolved; 0 with an open frontier; 1 reviewed against another environment +``` + +Three things about that line are deliberate: + +- **It is a rendering, not a finding.** Exit code stays `0`. Being handed a + record built elsewhere is legitimate; the only correct response is to say it + does not apply here. `conformance`'s **C-10 still FAILs** the same document, + and that is not a contradiction — C-10 asks whether the *producer* assembled a + coherent bundle, and one shipping a foreign-env review beside this environment + is incoherent. Producer and consumer are different questions. +- **`not_applicable` is counted on its own**, never folded into `reviewed` (that + would restate the hole as a statistic) and never into the unreviewed remainder + (that would lose the fact that a human has already read these — the cheapest + work in the queue). +- **Without `--environment`, review columns read `not_run`**, and `join` says on + stderr why. Applicability cannot be established, so the axis does not claim it + was. Rendering the verdict instead would reintroduce exactly the silent pass + this section exists to close; the cost of the other direction is an operator + passing one more flag, which is loud and recoverable. + +`not_applicable` is never `pass` and never `fail`. arXMCP's `CLAUDE.md` §4.10 +rule 3 binds the same rule from the other side of the seam. + +### Reviews join by digest, because a name-keyed join fails silently + +`review.decl` records a Lean name. Joining on it breaks under a rename: the +type is unchanged, so `reviewed_statement_digest` still matches while `decl` +dangles — and the join either loses the review (the axis silently reverts to +`not_run`) or, if it is lenient, floats it onto a different declaration. + +So the key is the digest and `decl` is a hint whose disagreement is itself +reported. The two failure modes are kept apart because their remedies differ: + +| what happened | `J-01` says | +|---|---| +| digest matches, name changed | nothing — this is a rename, and it is fine | +| digest misses, `decl` present | the statement was **restated** under the review | +| digest misses, `decl` absent | rename **and** restatement; a human must adjudicate | + +`J-03` refuses to merge disagreeing reviews of one statement. Deduping them +would pick a winner, and the point is that a person has to. + +### `J-06` computes the queue; `--workqueue-out` writes it down + +The work queue — every registry entry with **zero inbound citations**, +partitioned by `kind`, with each entry's open frontier rolled up — is the file +an agent plans against. The rule computes it, and hand it a registry document +and it runs: + +``` + FAIL J-06 the obligation lane: registry entries with no citation + stmt:9f4c1a20b7d3:b: kind='obligation', zero inbound cites; open frontier ['gltilde-universal-cover'] + (conjecture: 1, obligation: 2) +``` + +Counted **per kind and never totalled**. A queue of 90 entries in one lane and +10 in another is not "100 things to do", and a single total is the one number +that makes the file unplannable. + +`mfc join --registry … --workqueue-out attest/workqueue.json` writes that set as +`workqueue/1.0`, the ninth artifact: + +```json +{ + "schema_version": "workqueue/1.0", + "registry_id": "9f4c1a20b7d3", + "registry_sha256": "8c8ec3dd…", + "declarations_sha256": "0cfb36c2…", + "lanes": { + "obligation": { + "count": 1, + "entries": [ + { "key": "stmt:9f4c1a20b7d3:obl-stab-action", + "title": "Show the action is free", + "note": "Owed: no declaration yet asserts freeness…", + "frontier_open": ["gltilde-universal-cover"], + "depends_on": [] } + ] + } + } +} +``` + +**Why this may be written when `conformance` writes nothing.** The rule was +never "no files" — it was "no aggregate verdicts". A queue is an *inventory*: it +records what is owed, judges nothing, and has no axis to collapse. There is no +field it could carry that would make one, and `test_the_queue_is_an_inventory_and_never_a_verdict` +holds it to that. + +**Why it did not have to wait for the size-ceiling decision.** The stated +blocker was that partitioning by `kind` would bake an unmade decision (is there +a zero-axis `sketch` lane?) into a schema. It does not have to: `lanes` is keyed +by whatever kind actually appeared, with `propertyNames` a *pattern* rather than +an enum of the ten `registry/1.0` knows. Adding a member there is a one-schema +MINOR bump, and the two copies cannot disagree because there is only one. +`test_lanes_are_not_a_second_copy_of_the_kind_enum` puts a `sketch` lane through +`mfc validate` today, before the decision exists. + +**No timestamp**, so the file is byte-reproducible from two digested inputs and +`git diff --exit-code attest/` means something. Lanes are sorted, so a lane +appearing or emptying moves one hunk instead of reshuffling the file. + +Refused rather than written empty without `--registry`: a queue with no lanes +and a queue nobody computed are different files, and only one of them means +nothing is owed. + +### The accessor was wrong for three rules at once + +`E-04`, the registry half of `E-05`, and `J-06` all read +`registry["statements"]` as a list of `{key, frontier}`. **No released schema +ever had that shape** — it was invented alongside the rules and then tested +against itself. `registry/1.0` keys `entries` **by citation key**, and +`frontier[]` holds objects whose open state is `discharged_by: null`. + +Two things that hid behind the wrong shape: + +* an entry whose frontier items are **all discharged** has nothing outstanding, + and `E-05` was refusing `relation_claimed: exact` on those. Length was never + the predicate. +* reading an unrecognised document as an *empty* registry makes `E-04` report + every citation in the repository as unknown while `J-06` reports a clean work + queue over zero entries — a finding flood and a vacuous pass out of one bad + input. So `mfc/registry.py` raises, and the callers turn that into `not_run` + with the reason. Same discipline as an unrecognised `.ilean` layout. + +## `check-ilean-coverage`: the only check that looks for what is *absent* + +Every other rule here reads the emission and asks whether what it contains is +allowed. A mis-scoped emitter produces a perfectly valid, perfectly lint-clean +emission over the wrong set of modules, and every downstream artifact is then +immaculate and incomplete. + +`lake build` writes one `.ilean` per module beside the `.olean`, listing the +source-written declaration names. It is plain JSON, and it is produced by Lake +rather than by us — the one description of "what was built" that does not come +from the emitter. + +### Why it is not circular + +The emission carries a `modules[]` array computed by the emitter's own +`inScopeModules`. Comparing `.ilean` files against *that* would check the +emitter against itself: a scope bug drops a module from `modules[]` **and** +from `constants[]`, leaving the emission perfectly self-consistent. So the +in-scope set is re-derived from the filesystem using only the **declared** +`root_lib` (which `--lib` overrides), and `I-04` compares the two derivations. +`test_i04_catches_a_scope_bug_that_a_self_comparison_cannot` is the test that +holds the line. + +### Module prefixes are components, never strings + +`"TopicTest".startswith("Topic")` is `True`, and `TopicTest` is not a submodule +of `Topic`. A string prefix pulls the sibling test library into scope, and then +the coverage check fails on declarations the emitter is *correct* to exclude. +Measured on this repo: 6 built modules, 3 in scope, 29 in-scope declarations, +0 missing — with `MathFormalContractTest` and both executables correctly out. + +### The bootstrap is solved a level up, and that changed what E-08 is for + +Writing this surfaced something about the existing design. #31 warns that a +zero-declaration first build would fire the guard and stop any adopter reaching +a first green build. It cannot: `emission-1.0.schema.json` sets +`constants: minItems 1` and `counts.total/in_scope: minimum 1`, so an empty +emission is **not a representable artifact**, and every subcommand validates +before it reads. + +Which means `E-08`'s counts half — documented above as the vacuous-pass rule — +is **unreachable through any `mfc` subcommand**. The `empty-emission` fixture +is rejected by `mfc validate`, not by `E-08`; its test calls `check()` directly +and so never noticed. That is the *right* arrangement, and the same one +`additionalProperties: false` gives the trust-token ban — a structural +guarantee beats a rule that a caller can skip. But it was credited to the wrong +mechanism, so both are now labelled for what they are, and +`test_an_empty_emission_is_not_a_representable_artifact` pins the schema +constraint so that relaxing it becomes a visible decision rather than a silent +transfer of responsibility to a rule nothing runs. + +The half that no `minItems` can see is the **partial** sweep, and that is what +this command is for. No `--allow-empty` flag exists, deliberately: it would +collapse "genuinely empty repository" and "mis-scoped emitter" into one state, +which is the exact failure the check exists to prevent. They are already +distinct — `.ilean` carrying declarations while `constants[]` is empty is the +bug; both empty is a fresh repo; **no `.ilean` at all is exit 2**, because a +mis-pointed build directory must never be reportable as full coverage. + +## `init`: the measure is a green build on run one + +The test of this command is not that it writes files. It is that the tree it +writes **passes the rest of `mfc` with no hand-editing** — because an adopter +whose first CI run is red learns nothing about their own work, and the most +likely thing they do next is delete the workflow. + +That constraint is sharper than it looks, and it connects directly to the +`minItems: 1` finding above: an emission over zero declarations is not a +representable artifact, so **the scaffold has to ship a real Lean +declaration**. `AnalyticNT/Basic.lean` carries one, with the reason written in +the file so it does not get tidied away. + +`test_the_generated_repository_survives_the_whole_chain` renders a repo, +`lake build`s it, runs its emitter, and then puts the result through `validate`, +`lint`, `check-ilean-coverage`, `bundle` and `join`. Mathlib is swapped for a +local path require, because the question is whether the *generated Lean* +compiles, not whether Lake can download. Measured on the real thing: builds in +14 jobs, emits 1 constant, `lint` 7 passed / 0 failed, coverage 5 passed / 0 +failed. + +That test is the only thing establishing the central claim, so **its skip is +refusable**: with `MFC_REQUIRE_LAKE=1` a missing `lake` is a failure rather than +a skip, and CI sets it in the job that has a toolchain. A skipped check reads +exactly like a passing one in a green run. + +### It renders files and nothing else + +No `git init`, no remote, no commit. A hand-initialised repository has no +remote, no CI permissions, no branch protection and no provisioning, and a tool +that quietly produced one hands you something that looks finished and is not. +`mfc init` prints what it did *not* do, in order, and refuses a non-empty +directory without `--force` — the first thing it would otherwise overwrite is a +`lakefile.toml` somebody wrote. + +Every pin must be 40-hex. A branch is refused because `lake update` re-resolves +it, so the pin would stop pinning with nothing in the repo changing to show it. + +### Rendered with the standard library, not copier — and when to revisit + +The architecture note specifies copier, and its `copier update` is the stated +migration path for a MAJOR schema bump across N topic repos. That is a real +benefit with, today, **no users**: one topic repo exists and it was not created +from a template, so there is nothing for `copier update` to update. Against it, +copier pulls jinja2, pydantic, plumbum and questionary into a package that +argues its own placement decisions from dependency discipline. + +So the templates are plain text with `@@TOKEN@@` substitution — over +`str.format` and `string.Template` because Lean uses both `{}` and `$`, and a +scaffolder that mangles the file it writes is worse than none. A test asserts +no rendered file carries a live token, and the renderer refuses rather than +shipping one. + +**Reversal condition:** adopt copier when a second topic repo exists, *was +created by this command*, and a MAJOR schema bump is due. These files become +the template with the tokens rewritten to `{{ }}`. + +## `registry`: the only hand-authored artifact + +Everything else here is emitted by a program and recomputed by another one. The +registry is typed by a person, at 20–40 minutes an entry, so its rules are +about the mistakes typing makes. + +`registry-1.0.schema.json` was **transcribed** from the design note rather than +authored, the same discipline `digest.py` used — it was given in full there, and +it turned out to be blocked on nothing. The open size-ceiling decision adds an +enum member (a MINOR bump) and a policy; neither moves a shape. + +```bash +mfc registry init # mint a 12-hex id, once per repository +mfc registry validate registry/foo.yaml --frontier-kind-labels mathlib-gap +``` + +The two rules that carry the most weight: + +* **`R-02` recomputes `quote_sha256` from the inline text.** Without it the + digest is a number somebody typed — and `registry_sha256`, the entire + cross-repo freshness mechanism, is built from digests that were never checked + against what they summarize. It is whitespace-insensitive, like the digest + it uses, so a re-wrap does not rotate every citation. +* **`R-06` refuses a key shaped like a corpus id.** A `chunk_id` is exactly what + a corpus hands you, so someone will paste one in — and chunk ids *rotate* on + re-parse with no alias table, so the citation silently stops resolving while + the old id stays addressable. `@[cites]` rejects the shape at compile time + too; both, deliberately, because a hand-edited YAML file never passes through + Lean. + +### Two of the nine were already structural + +The design note tables these as *"rules over the registry that JSON Schema +cannot express."* True of seven. Running the fixtures through the CLI showed it +is **not** true of `R-01` and `R-06`: `source.version` carries +`pattern: ^v[0-9]+$` at the property level, and `entries` carries +`propertyNames: {$ref: citationKey}`. Both fixtures fail `mfc validate` before +`mfc registry validate` reaches the rule. + +Same shape as `E-08`, and the same answer: the structural guarantee is the +stronger arrangement, the rules stay as backstops for a caller that skipped +validation, and `SCHEMA_ENFORCED` in the tests asserts *which layer catches +which* rather than letting a fixture pass the suite while proving nothing. + +### One thing the transcription got wrong, and the fix + +Transcribing the note faithfully preserved a defect the note's own issue (#21) +had already identified: `mint_resolution` was schema-**required** and non-empty +for every kind but `obligation`, so **no entry could be minted until a resolver +existed** — and standing up the resolver is a later migration step. An adopter +with no corpus running could not create their first entry. + +Relaxed as the issue asks, to optional-with-reason: any kind may carry +`mint_resolution: null`, and a null **must** carry `mint_unresolved_reason`. +That is the `not_run` discipline one level down — *nobody asked the corpus* and +*the corpus had no answer* are different facts, and neither may present as +*matched*. Expressible in JSON Schema, so it is structural rather than an +`R` rule, and it has a rejection fixture like everything else. + +Amended in `registry/1.0` rather than minted as `1.1`: the schema landed in the +same session and nothing consumes it yet. + +### The fixtures carry no marker key + +Unlike `artifacts/invalid/`, the registry rejection fixtures have no +`$comment_fixture`. `additionalProperties: false` would reject the marker +rather than the defect, and the fixture would never reach the rule under test — +green suite, nothing proved. The rationale lives in +`testdata/registries/invalid/README.md`, and every fixture is a document that +validates against the schema and fails on exactly one content rule. + +## `bundle` recomputes; it does not carry anything across + +The emission is produced by the topic repo's own emitter in the topic repo's +own build. It is an **input**, not a source of truth. So `axioms` is re-sorted +and re-deduped, `contains_sorry_ax` is recomputed from that list, `counts` are +recounted from `constants[]`, and `axioms_disallowed` is derived from the +environment's `axiom_policy` — a field the emission deliberately does not +report at all, so there is no value to disagree with. + +This is not suspicion of the emitter. It is that a producer reporting its own +verdict has one failure mode no amount of care removes, and the contract exists +to keep that failure mode out. There is no code path here that emits a clean +`axioms_disallowed` for a declaration whose axioms contain `sorryAx`. + +Both inputs are validated **before** anything is derived from them, and the +output is validated **before** it is written — `mfc` must not be able to emit +an artifact its own schema rejects. + +## Digests are pinned by data, not by agreement with ourselves + +`digest.py` is frozen: any change is a MAJOR bump on every artifact carrying a +digest. `tests/test_digest.py` reproduces the three values the design note +recorded as `[COMPUTED]` against the real repository at `f166a3d` — the +`env_digest` and both statement digests — so a refactor that changes key order, +separators, or the NFC-then-collapse order fails immediately. + +That matters more here than usual. The fixture corpus lives inside one of the +implementations it referees, so "our code agrees with our code" proves nothing; +agreement with values computed before this code existed does. It is red-team +gap 16's mitigation. + +The properties those digests encode, each with its own test: + +* a **def's body is part of its statement** — two defs with one type and + different bodies are different claims; +* a **theorem's proof is not** — folding it in would make every proof edit read + as a statement change, destroying the signal review depends on; +* a **rename does not rotate** anything — citations anchor to a registry key; +* **re-wrapping does not rotate** anything — `type_pp` carries hard line breaks + at the pinned `format.width`. + ## `validate`, and why it does not take a `--schema` Every artifact carries `schema_version` as its first key, and `validate` reads diff --git a/contract/mfc.egg-info/SOURCES.txt b/contract/mfc.egg-info/SOURCES.txt index 186a222..ad7da6a 100644 --- a/contract/mfc.egg-info/SOURCES.txt +++ b/contract/mfc.egg-info/SOURCES.txt @@ -1,20 +1,61 @@ README.md pyproject.toml ./mfc/__init__.py +./mfc/bootstrap.py +./mfc/build.py +./mfc/bundle.py ./mfc/cli.py +./mfc/conformance.py +./mfc/containment.py +./mfc/digest.py +./mfc/env.py +./mfc/freshness.py +./mfc/ilean.py +./mfc/join.py ./mfc/lint.py +./mfc/registry.py +./mfc/restate.py +./mfc/review.py +./mfc/rules.py +./mfc/rules_registry.py +./mfc/scaffold.py +./mfc/seal.py ./mfc/validate.py +./mfc/withdrawals.py ./mfc/schema/build-1.0.schema.json ./mfc/schema/bundle-1.0.schema.json ./mfc/schema/declarations-1.0.schema.json ./mfc/schema/emission-1.0.schema.json ./mfc/schema/environment-1.0.schema.json +./mfc/schema/registry-1.0.schema.json ./mfc/schema/resolution-1.0.schema.json +./mfc/schema/restate-1.0.schema.json ./mfc/schema/review-1.0.schema.json +./mfc/schema/run-1.0.schema.json +./mfc/schema/withdrawals-1.0.schema.json +./mfc/schema/workqueue-1.0.schema.json mfc/__init__.py +mfc/bootstrap.py +mfc/build.py +mfc/bundle.py mfc/cli.py +mfc/conformance.py +mfc/containment.py +mfc/digest.py +mfc/env.py +mfc/freshness.py +mfc/ilean.py +mfc/join.py mfc/lint.py +mfc/registry.py +mfc/restate.py +mfc/review.py +mfc/rules.py +mfc/rules_registry.py +mfc/scaffold.py +mfc/seal.py mfc/validate.py +mfc/withdrawals.py mfc.egg-info/PKG-INFO mfc.egg-info/SOURCES.txt mfc.egg-info/dependency_links.txt @@ -26,8 +67,40 @@ mfc/schema/bundle-1.0.schema.json mfc/schema/declarations-1.0.schema.json mfc/schema/emission-1.0.schema.json mfc/schema/environment-1.0.schema.json +mfc/schema/registry-1.0.schema.json mfc/schema/resolution-1.0.schema.json +mfc/schema/restate-1.0.schema.json mfc/schema/review-1.0.schema.json +mfc/schema/run-1.0.schema.json +mfc/schema/withdrawals-1.0.schema.json +mfc/schema/workqueue-1.0.schema.json +tests/test_allowlist.py +tests/test_bootstrap.py +tests/test_build.py +tests/test_bundle.py +tests/test_conformance.py +tests/test_containment.py +tests/test_digest.py +tests/test_digest_corpus.py +tests/test_discharges.py +tests/test_env.py +tests/test_external.py +tests/test_freshness.py +tests/test_ilean.py +tests/test_join.py tests/test_lint_schemas.py +tests/test_multiroot.py +tests/test_quote_mode.py +tests/test_referent.py +tests/test_registry.py +tests/test_restate.py +tests/test_review.py +tests/test_rules.py +tests/test_rules_registry.py +tests/test_scaffold.py tests/test_schemas.py -tests/test_validate.py \ No newline at end of file +tests/test_seal.py +tests/test_validate.py +tests/test_vocabulary.py +tests/test_volatile.py +tests/test_withdrawals.py \ No newline at end of file diff --git a/contract/tests/test_lint_schemas.py b/contract/tests/test_lint_schemas.py index c90fc7c..76faeee 100644 --- a/contract/tests/test_lint_schemas.py +++ b/contract/tests/test_lint_schemas.py @@ -113,3 +113,53 @@ def test_unreadable_schema_is_usage_error_not_findings(tmp_path: Path) -> None: """Malformed JSON means the check did not run — exit 2, never 0.""" (tmp_path / "broken.schema.json").write_text("{ not json", encoding="utf-8") assert main(["lint-schemas", "--schema-dir", str(tmp_path)]) == EXIT_USAGE + + +# --------------------------------------------------------------------------- +# The installed package, against the source tree it was built from. +# --------------------------------------------------------------------------- + +def test_the_installed_schemas_are_the_source_schemas() -> None: + """A wheel that ships a stale schema validates the wrong contract. + + ADR-0009 makes `mfc` a SHARED tool: the topic repo and arXMCP both install + it, and what they install is the only copy they see. CI already installs + the package rather than running it from the tree, for exactly this reason + -- but "it installed" is a weaker claim than "it installed THIS". + + The failure is not hypothetical. `contract/build/` was in `.gitignore` + from the commit that introduced packaging, and eleven files under it were + committed in that same commit, before the ignore could take effect. + `.gitignore` does not untrack what is already tracked, so a fresh checkout + carried a `build/lib/` holding 2026-era copies of `cli.py`, `lint.py`, + `validate.py` and five schemas -- and setuptools' `build_py` copies a + source file into `build/lib` only when it is NEWER, which on a fresh + checkout it need not be. Observed: a `pip install ./contract` that shipped + a `resolution-1.0.schema.json` predating `not_applicable`, so a resolver + emitting a valid document was told its own output was invalid. + + Byte-identity, not "both parse": a schema can differ by a `$comment` that + changes nothing and by an enum member that changes everything, and only + one of those is visible to a diff of parsed structure. + """ + import mfc # the INSTALLED package + + installed = Path(mfc.__file__).resolve().parent / "schema" + source = Path(__file__).resolve().parent.parent / "mfc" / "schema" + if installed == source: + pytest.skip( + "`mfc` resolves to the source tree, so there is no installed copy " + "to compare against; CI installs the package and does the real run" + ) + src_files = sorted(p.name for p in source.glob("*.schema.json")) + inst_files = sorted(p.name for p in installed.glob("*.schema.json")) + assert src_files == inst_files, "the wheel shipped a different schema SET" + stale = [ + name for name in src_files + if (installed / name).read_bytes() != (source / name).read_bytes() + ] + assert not stale, ( + f"the installed mfc ships stale schema(s): {stale}. Delete " + f"contract/build/ and reinstall; if that fixes it, something is " + f"tracking build output again." + ) From ab8211e5c65ab9aae8903610ecc67023397643bf Mon Sep 17 00:00:00 2001 From: Chris Dare Date: Thu, 3 Sep 2026 23:12:38 -0400 Subject: [PATCH 4/4] The same defect, one directory over: *.egg-info/ was tracked too `*.egg-info/` is in `.gitignore` beside `/contract/build/` and was tracked for the same reason -- committed in the packaging commit, before the ignore could take effect. Ten files, including a `contract/UNKNOWN.egg-info/` left behind by a build that ran before the project had a name. Less dangerous than the stale schemas: nothing reads `SOURCES.txt` to decide what a contract means. But every `pip install ./contract` rewrites `PKG-INFO` and `SOURCES.txt` in place, so the tree goes dirty on any build and each run offers the diff up for staging. The previous commit swept two of them in exactly that way. Deleted from the index only; the directories stay on disk and stay ignored. --- contract/UNKNOWN.egg-info/PKG-INFO | 10 - contract/UNKNOWN.egg-info/SOURCES.txt | 6 - .../UNKNOWN.egg-info/dependency_links.txt | 1 - contract/UNKNOWN.egg-info/top_level.txt | 1 - contract/mfc.egg-info/PKG-INFO | 1025 ----------------- contract/mfc.egg-info/SOURCES.txt | 106 -- contract/mfc.egg-info/dependency_links.txt | 1 - contract/mfc.egg-info/entry_points.txt | 2 - contract/mfc.egg-info/requires.txt | 7 - contract/mfc.egg-info/top_level.txt | 1 - 10 files changed, 1160 deletions(-) delete mode 100644 contract/UNKNOWN.egg-info/PKG-INFO delete mode 100644 contract/UNKNOWN.egg-info/SOURCES.txt delete mode 100644 contract/UNKNOWN.egg-info/dependency_links.txt delete mode 100644 contract/UNKNOWN.egg-info/top_level.txt delete mode 100644 contract/mfc.egg-info/PKG-INFO delete mode 100644 contract/mfc.egg-info/SOURCES.txt delete mode 100644 contract/mfc.egg-info/dependency_links.txt delete mode 100644 contract/mfc.egg-info/entry_points.txt delete mode 100644 contract/mfc.egg-info/requires.txt delete mode 100644 contract/mfc.egg-info/top_level.txt diff --git a/contract/UNKNOWN.egg-info/PKG-INFO b/contract/UNKNOWN.egg-info/PKG-INFO deleted file mode 100644 index 405ec6f..0000000 --- a/contract/UNKNOWN.egg-info/PKG-INFO +++ /dev/null @@ -1,10 +0,0 @@ -Metadata-Version: 2.1 -Name: UNKNOWN -Version: 0.0.0 -Summary: UNKNOWN -Home-page: UNKNOWN -License: UNKNOWN -Platform: UNKNOWN - -UNKNOWN - diff --git a/contract/UNKNOWN.egg-info/SOURCES.txt b/contract/UNKNOWN.egg-info/SOURCES.txt deleted file mode 100644 index 1d0a9a7..0000000 --- a/contract/UNKNOWN.egg-info/SOURCES.txt +++ /dev/null @@ -1,6 +0,0 @@ -README.md -pyproject.toml -UNKNOWN.egg-info/PKG-INFO -UNKNOWN.egg-info/SOURCES.txt -UNKNOWN.egg-info/dependency_links.txt -UNKNOWN.egg-info/top_level.txt \ No newline at end of file diff --git a/contract/UNKNOWN.egg-info/dependency_links.txt b/contract/UNKNOWN.egg-info/dependency_links.txt deleted file mode 100644 index 8b13789..0000000 --- a/contract/UNKNOWN.egg-info/dependency_links.txt +++ /dev/null @@ -1 +0,0 @@ - diff --git a/contract/UNKNOWN.egg-info/top_level.txt b/contract/UNKNOWN.egg-info/top_level.txt deleted file mode 100644 index 8b13789..0000000 --- a/contract/UNKNOWN.egg-info/top_level.txt +++ /dev/null @@ -1 +0,0 @@ - diff --git a/contract/mfc.egg-info/PKG-INFO b/contract/mfc.egg-info/PKG-INFO deleted file mode 100644 index 52821bc..0000000 --- a/contract/mfc.egg-info/PKG-INFO +++ /dev/null @@ -1,1025 +0,0 @@ -Metadata-Version: 2.4 -Name: mfc -Version: 0.1.0 -Summary: Schemas and tooling for the math-formalization contract -Author: Chris Dare -License: MIT -Keywords: lean,formalization,provenance,json-schema -Requires-Python: >=3.11 -Description-Content-Type: text/markdown -Requires-Dist: jsonschema>=4.18 -Provides-Extra: yaml -Requires-Dist: PyYAML>=6; extra == "yaml" -Provides-Extra: test -Requires-Dist: pytest>=7; extra == "test" - -# `contract/` — the schemas, and the tooling that polices them - -The machine-readable half of the contract between a corpus of papers and a Lean -formalization of results from it. The Lean half — `@[cites]` and the emitter — -is the rest of this repo. - -## Why it lives here - -[`ADR-0009`](https://github.com/chris-dare-dev/bridgeland-stab-lean/blob/main/.claude/decisions/ADR-0009-contract-package-lives-with-the-emitter.md), -which replaced ADR-0007 after the latter's cited evidence was found not to -exist. Short version: this is the only candidate location whose justification -survives contact with the disk, arXMCP's own constitution says it does not host -formalization work, and the schema for `emission/1.0` now sits in the same -commit as the emitter that produces it. - -**The zero-dependency invariant is untouched.** It is about the *Lake* package — -`lakefile.toml` carries no `[[require]]`, and CI enforces that by grepping that -file. JSON and Python appear in neither. If anyone ever adds a Lake `require` -to serve this directory, the named exception in the consuming repo's -`CLAUDE.md` §1 lapses and the dependency comes out of every topic repo. - -## What is here today - -| path | what | -|---|---| -| `mfc/schema/*.schema.json` | **all twelve** artifact formats | -| `mfc/digest.py` | the four canonical digest functions — **frozen** | -| `mfc/lint.py` | the banned-property lint, and the volatile-property lint | -| `mfc/validate.py` | artifact validation | -| `mfc/bundle.py` | `declarations.json`, everything recomputed | -| `mfc/build.py` | `build/1.0` from lake's NDJSON — the sorry count comes from `kind`, never the exit code | -| `mfc/seal.py` | `bundle/1.0`, the in-toto Statement `conformance` reads | -| `mfc/rules.py` | the E-01..E-10 content rules | -| `mfc/bootstrap.py` | the write-once `bootstrap` flag — how a repo with nothing in it yet reaches a first green build | -| `mfc/conformance.py` | the C-01..C-12 cross-artifact rules | -| `mfc/join.py` | the J-01..J-06 rules and the claim table | -| `mfc/ilean.py` | the I-01..I-05 coverage rules | -| `mfc/registry.py` | reading a `registry/1.0` document | -| `mfc/rules_registry.py` | the R-01..R-09 registry rules | -| `mfc/scaffold.py` | `mfc init` — the topic-repo templates | -| `mfc/env.py` | `mfc env` — reads a topic checkout, writes `environment/1.0` | -| `mfc/cli.py` | `mfc lint-schemas`, `validate`, `bundle`, `build`, `lint`, `conformance`, `seal`, `join`, `env`, `check-ilean-coverage`, `init`, `registry` | -| `pyproject.toml` | packaging, so a consumer can install it | -| `testdata/schemas/invalid/` | schemas that must fail the lint | -| `testdata/artifacts/valid/` | one filled instance per schema | -| `testdata/emissions/bootstrap/` | the emission a repository has *before* it has any mathematics | -| `testdata/artifacts/invalid/` | artifacts that must fail a cross-field rule | -| `testdata/registries/invalid/` | registries that must fail an `R` rule | -| `testdata/digests/` | the canonical **bytes** behind nine digests, hand-written and hashed with `shasum` | -| `tests/` | pytest | - -### How much of each schema was given, and how much was authored - -Only `emission` was fully copy-pasteable from the design note. This matters for -review: the rest are **authored**, and authoring can drift from intent in a way -transcription cannot. - -| schema | source | check that it did not drift | -|---|---|---| -| `emission` | full JSON | fixture is trimmed **real emitter output** | -| `review` | near-full JSON, missing only the wrapper | accepts the note's instance | -| `resolution` | `$defs.result` full; envelope inferred from the instance | accepts the note's instance | -| `declarations` | instance + one `allOf` fragment | accepts the note's instance | -| `build` | instance + one `if/then` fragment | accepts the note's instance | -| `environment` | instance + prose bullets, no JSON | accepts the note's instance | -| `bundle` | instance + prose bullets, no JSON | accepts the note's instance | - -### The rules that carry the trust model - -Every `allOf` in these schemas encodes a trust rule, not a formatting -preference, and each has a fixture that must be **rejected** — a conditional -that never fires is indistinguishable from one that is not there: - -| fixture | what it smuggles | -|---|---| -| `sorry-laundered` | `sorryAx` in `axioms` while `contains_sorry_ax` is false | -| `fuzzy-current` | a fuzzy match claiming `current` — similarity is not identity | -| `current-without-digest` | `current` without the recomputed body digest | -| `exact-with-divergence` | `relation_confirmed: exact` alongside a divergence | -| `divergent-without-divergence` | a divergent verdict that does not say how | -| `checker-pass-allow-sorry` | a checker that passed *while permitting* sorry | -| `aggregate-verdict` | an SLSA-style `verificationResult` on the bundle | - -The last one is why `additionalProperties: false` is everywhere rather than -just tidy: it is what stops a single collapsed trust token being added to an -artifact at all. - -### `run/1.0`: the artifact that exists in order not to be committed - -`git diff --exit-code attest/` is the only one of the four claimed sorry-gates -that survives the seam. Two separate things were wrong with it. - -**It could never pass.** `bundle.json` carried `produced_at` on every -predicate; `build.json` carried `produced_at` and `ci{run_url, workflow_sha, -runner}`. Both are committed, both changed on every run, so the gate went red -on no-op commits — and a gate that is red on no-op commits gets deleted within -the week, by someone who is right that it is broken and wrong about which half -to remove. - -**It could never fail either.** The generated `.gitignore` ignored -`/attest/*.json` wholesale, so the diff compared nothing at all. Fixing only -the first half would have produced a gate that passes for the wrong reason, -which is indistinguishable from the bug. - -Both are fixed. Everything that changes per run moved to `run/1.0` — -`attest/run.json`, gitignored, shipped as a release asset — and it names the -files it produced by `sha256`, so provenance still joins back to the committed -tree without anything in the committed tree moving. `contract_repo` stayed in -the bundle: `rev` is a **pin**, and a pin that changed every run would not be -pinning anything. - -`mfc lint-schemas` now fails on a `produced_at` in any of `declarations`, -`environment`, `bundle`, `build` — the four artifacts CI regenerates on every -commit and commits the result of. It does **not** police `review.reviewed_at` -or `resolution.generated_at`: those are committed, but they are written by a -deliberate human or offline act, and the date a person reviewed a statement is -the fact being recorded rather than run metadata. Banning them would delete -evidence to protect a gate they do not threaten. - -### Canonicalization is pinned by data, because there is only one implementation - -JSON-Schema-Test-Suite works because ~20 independent implementations run the -corpus. Here there is one, so "our code agrees with our code" proves nothing: a -canonicalization bug is symmetric and invisible to conformance. - -`testdata/digests/canonicalization.json` carries, for each of the nine cases, -the **exact bytes** fed to `sha256` — written by hand from the spec in -`digest.py` and hashed with `shasum(1)` — beside the digest of those bytes. -The tests then assert the datum is internally consistent using stdlib `hashlib` -alone, that `mfc` reproduces those bytes **byte for byte**, and that the -end-to-end digest matches. Under drift the first still passes and the second -fails, naming the bytes that moved. - -Three of the nine reproduce values the design note recorded as `[COMPUTED]` -against the real repository at `f166a3d`, months before this code existed — -hand-written canonical forms whose `shasum` matched numbers nobody could have -back-fitted. A fourth test set mutates the canonicalizer three plausible ways -(unsorted keys, default separators, `ensure_ascii=False`) and asserts each is -rejected, because assertions that cannot fail are the thing being fixed. - -The rule for adding a case is in `testdata/digests/README.md` and is one line: -never paste `mfc`'s own output. - -### One judgement call worth flagging - -The note's filled instances carry `$comment` keys as reader documentation. -Those are **not** in the schemas, so a real artifact may not contain them — -they were annotations for a human, not fields. If they were meant to survive -into the artifacts, the schemas need `$comment` allowed explicitly. - -## Installing and running it - -```bash -pip install ./contract # from the repo root -pip install './contract[yaml]' # adds attest/review.yaml support - -mfc lint-schemas # works from any directory once installed -mfc validate attest/lean-emission.json -``` - -ADR-0009 made `mfc` a **shared** tool — "rule 7", which had confined it to the -corpus server's side, came from the document that does not exist. So a topic -repo installs this rather than vendoring schema copies with a checksum-drift -test, and the drift problem vendoring solved does not arise while the schemas -and the emitter share a repo and a commit. - -Two placement notes, both deliberate: - -* **`pyproject.toml` is under `contract/`, not at the repo root.** The root is a - Lake package; a `pyproject.toml` beside `lakefile.toml` invites tooling on - either side to treat the other's tree as its own. -* **The schemas live inside the package**, at `mfc/schema/`. An installed CLI - that cannot find its schemas is useless. They are still plain JSON at a - stable, greppable path for any non-Python consumer. - -Neither adds a Lake dependency, so the zero-dependency invariant is untouched. - -## `lint`: a rule that did not run is not a rule that passed - -Schema validation says an artifact is well *formed*. The E-rules say whether -what it contains is *allowed* — a perfectly well-formed emission can still -launder a `sorry`, declare an undeclared axiom, or cite a key that does not -exist. - -Two rules cannot run yet. `E-04` needs the statement registry, which is gated -on the open size-ceiling decision, and `E-09` needs the topic's `closed_lanes` -configuration. They report **`not_run`**, never `pass`, and every invocation -prints which rules did not run instead of folding them into a count: - -``` -7 passed, 0 failed, 3 not_run -note: E-04, E-05, E-09 did NOT run. This is not a pass -- nothing checked - what they check. -``` - -That is the trust-axis rule applied one level down. A green lint with -`E-04: not_run` must not be readable as "the citations resolve". `--require-all` -turns any `not_run` into a failure, for the day the inputs exist. - -`E-05` shows the other half of the idea: its emission half (a citation claiming -`exact` while carrying its own open frontier) runs now and *fails* now; only -the registry half is deferred. A missing input suppresses exactly what it must -and no more. - -Every rule has a fixture in `testdata/emissions/invalid/` that must trip it. - -### The bootstrap flag, and why it burns down - -The vacuous-pass guard is structural: `emission-1.0.schema.json` sets -`constants: minItems 1` and `counts.total/in_scope: minimum 1`, so an empty -emission is not a representable artifact. That also made an adopter's **first** -build unreachable — a repository generated by `mfc init` has no declarations, -and the generated workflow emits before anything has been written. - -`formalization.yaml` carries `bootstrap: true`. While it is set, `validate`, -`bundle` and `lint` accept an empty emission against a copy of the schema with -exactly three constraints dropped (`bootstrap.RELAXED`, asserted by test to be -the only difference), and every E-rule reports **`not_run`** — a green table -over an empty emission would otherwise say "no declaration depends on -`sorryAx`" about a repository with no declarations. - -Three properties keep it from being an `--allow-empty` flag with a longer name: - -- **It burns down.** `mfc lint` clears it the first time it sees in-scope - declarations and stamps `bootstrap_cleared_at`. A record carrying that date - may never set `bootstrap: true` again — `bootstrap.read` raises on the - combination rather than honouring it. -- **It excuses one situation, not two.** An emission with constants and - `counts.in_scope: 0` is a *mis-scoped emitter*, and that is a defect on day - one exactly as it is on day one thousand. Bootstrap does not touch it. -- **A broken emission cannot burn it.** Clearing needs in-scope declarations, - not merely "not empty", so a bad emitter run cannot cost a repository its - bootstrap state permanently. - -The cleared record is left in the working tree for the operator to commit, -which is what `git diff --exit-code attest/`-style gates are for: clearing the -flag is a commit someone makes, not a fact CI invents. - -**`E-07` earns its keep twice.** It was written so two different statements -cannot hash identically. It also turns out to select exactly the statements -that cannot be re-elaborated — measured at 339/339 round-trip on elision-free -statements and 0/61 on elided ones — so it is already the precondition -`--restate-check` needs. - -## `env`: the record everything consumed and nothing produced - -`bundle` stamps `env_digest` onto declarations. `conformance` checks `C-05` and -`C-10` against it. `join` renders a review `not_applicable` when it disagrees. -All three read an `environment/1.0` record — and until now **nothing wrote one.** -In this repository's own CI the real emission is bundled against -`testdata/artifacts/valid/environment-1.0.json`, a *fixture*: the one artifact -meant to pin what the measurement was made in was describing a different machine. - -```bash -mfc env --repo ../topic-repo --out attest/environment.json \ - --axiom-allowlist propext,Quot.sound,Classical.choice \ - --emitter-version mfc-emit/1.0.0 -``` - -Every field is read out of the checkout — `lean-toolchain`, -`lake-manifest.json`, `lakefile.toml`, `git`. Two are inputs rather than -observations, and deliberately so: - -* **`axiom_policy`** is a policy, not a property of a build. Defaulting it would - be this package asserting a policy on a topic repo's behalf, so it is - required — the same reasoning that makes `@[cites]`'s `relation` mandatory. -* **`lean_githash` / `lake_version`** come from running the toolchain, and are - overridable so a caller without one on PATH supplies what it measured rather - than receiving a fabricated value. - -### What it says out loud - -Run against the consuming repo it reports, correctly and unprompted: - -``` - NOT PINNED 13 package(s) track a branch and would move on `lake update`: - Cli, LeanSearchClient, MD4Lean, Qq, aesop, batteries, importGraph, - informal, mathlib, plausible, proofwidgets, subverso, verso - UNTAGGED valid artifact, invalid release -- a release pin requires a tag -``` - -Thirteen of fifteen, **mathlib among them**. That is why `env_digest` hashes -`rev` and never `inputRev`: `inputRev` is what a caller asked for, `rev` is what -resolved, and hashing the ask would leave the digest stable across a real -environment change. `test_changing_input_rev_alone_does_not_move_the_digest` -pins that, with `test_changing_a_resolved_rev_does_move_the_digest` as its -control. - -A dirty worktree is **recorded, not refused** — refusing would make the tool -unusable mid-work, and dropping it would let a digest describe a tree that is -not in git. `mfc lint` is where dirty becomes fatal, in CI mode. - -A package with no resolved 40-hex `rev` is refused outright rather than -placeholdered: an unpinnable dependency inside a digest that claims to pin -everything is worse than no artifact. - -### It will not run against this package - -`mfc env --repo .` here fails with *"'MathFormalContract' is not in -lake-manifest.json"*, and that is correct. This is a leaf with no manifest -packages — it is the contract package, not a topic repo. Which also means this -repo's own CI cannot produce a real environment record for itself, and its use -of the fixture is a test of the emitter rather than a trust record. Read it that -way. - -## `build`: the exit code is not the measurement - -`lake env lean --json` on a file whose only defect is a `sorry` **exits 0**. -Measured on `leanprover/lean4:v4.32.1`, the pinned toolchain: - -``` -{"kind":"hasSorry","severity":"warning","data":"declaration uses `sorry`",...} -EXIT=0 -``` - -So `lake_build_exit` is recorded and never consulted, and the gate is -`sorry_diagnostic_count`, counted from records whose `kind` is `hasSorry`. This -is the emitter's "never parse the source" discipline one level down: in the -build log rather than in the declaration. - -Counting by `kind` has one silent failure mode — a toolchain that renames or -drops the tag turns every sorry into an uncounted warning and the count reads -`0`. A diagnostic whose *text* reads like a sorry while its `kind` says -otherwise is therefore a **hard failure**. The text is a tripwire and never the -counter: counting from prose would break the moment Lean rewords the message, -which is why the `kind` field exists at all. - -A line that is not a JSON object raises rather than being skipped. A diagnostic -that could not be parsed is a diagnostic that would not be counted, and an -undercount is indistinguishable from a clean build — so lake's human-readable -progress output on the same handle is reported as the caller error it is. - -`independent_checkers` is an input, not an observation, for the same reason -`axiom_policy` is: this package cannot know what else was run. An empty array -reads as "none was run", which is different from the field being absent. - -### `measured`: a clean build and an unmeasured build are the same document - -`error_count`, `warning_count` and `sorry_diagnostic_count` are all `0` whether -the build was spotless or the NDJSON covered one module of 494, and no other -field in `build/1.0` can tell those apart. That makes an unmeasured build the -most flattering artifact this package could write — the same absence -`check-ilean-coverage` exists for, one level down in the build log. - -It is not a hypothetical. Measured on `leanprover/lean4:v4.32.1`, there is no -cheap route to project-wide NDJSON: `lake env lean --json` on a root import -file prints **nothing**, because imports are served from oleans and never -re-reported; `moreLeanArgs = ["--json"]` is consumed by lake, which re-renders -messages in its own text format; lake persists no structured log under -`.lake/build`; and per-module invocation pays a full Mathlib import load each -time. A consumer repository's CI therefore measures a handful of modules, and -`measured` is what stops that reading as a clean sweep. - -Its numerator is **declared**, because a module that elaborated cleanly leaves -no trace in the log and cannot be recovered from it — `--covers MODULE`, or -`--covers-all` as a deliberate claim rather than a default. Its denominator is -**read from the emission's `modules[]`**, never from the caller, so the one -number that could be shrunk to flatter the other cannot be. A declared module -absent from that list is a hard failure: coverage may be narrow, and it may not -be invented. - -No ratio is stored. A reader divides two integers. A single `coverage: 100%` -would be the collapsed trust token every schema here refuses, and it would be -the first thing a tired reader believed. - -## `conformance`: seven valid artifacts that do not describe the same thing - -`validate` asks whether one artifact is well formed. `lint` asks whether one -emission contains anything forbidden. Neither can see the failure this command -exists for — a `build.json` measured before the last commit, a review performed -against an earlier environment, a `declarations.json` derived from an emission -other than the one shipped. Each file passes its own schema. The set is still a -lie. - -Twelve rules, all of them a link between two artifacts rather than a property of -one. `C-02` (a predicate's `sha256` is the file's actual bytes) is the load -bearer: without it every other link is between things the bundle merely -asserts. `C-07` is the only rule that checks a digest against the data it -summarizes rather than against another digest. - -### It writes no artifact, and that is the point - -The obvious shape is to emit `conformance.json` with a verdict in it. It -deliberately does not, because there is nowhere honest to put one — a -`conformance.json` carrying a top-level verdict *is* the `aggregate-verdict` -rejection fixture, mechanically produced by our own tool. - -Read that as "no aggregate verdicts", not "no files". `join --workqueue-out` -writes `workqueue/1.0` and does not breach this, because a work queue judges -nothing — see [`join`](#j-06-computes-the-queue-workqueue-out-writes-it-down). - -So the output is a report and an exit code, and the reviewable object is an -evidence table: - -``` -evidence - environment attest/environment.json mfc/1.0.0 self-attested this environment - human-review attest/review.json human:Chris Dare independent this environment - corpus-resolution attest/resolution.json arxmcp/statement_resolve.. independent n/a (not a Lean measurement) - provisional-self-reported attest/lean-verify-tran.. arxmcp/lean_verify@v4.31.0 self-attested OTHER environment (ffffffff...) - -6 predicate(s); 2 not self-attested; 1 produced in another environment -``` - -Three counts, printed separately and never combined, because "6 predicates" -must not be readable as "6 independent measurements of this build". No column -of that table is a score, and `test_no_row_carries_a_verdict` keeps it that way. - -### Out-of-environment evidence is labelled, not averaged in - -The reference bundle carries a transcript produced by a **v4.31.0** toolchain -against a repo pinned to **v4.29.0**. That is legitimate and must stay visibly -separate, which is what the `provisional-self-reported` predicate type is for. -`C-05` makes the label binding: a `build/v1` predicate carrying a foreign -`env_digest` is a measurement of another build presented as a measurement of -this one. - -There is one way to satisfy `C-05` without fixing anything — relabel the -predicate as provisional. That is the intended escape, not a hole: relabelling -*is* the retraction, and the table then shows a claim demoted to nothing. - -### Capturing `reviewed_statement_pp`, and why it proves itself - -`reviewed_statement_pp` is the string a review's survival depends on: -`restateOne` parses it, elaborates it, and asks `isDefEq` against the -declaration's current type. Every way of getting it wrong is **silent** — the -field looks captured, `mfc validate` passes, and the failure appears at the -next dependency bump as `not_checkable`, which reads like a broken tool rather -than a bad capture. - -Capturing the first real one by hand took three attempts: - -1. **Elision.** `pp.explicit` alone left a `⋯` inside a proof argument. - `pp.proofs`, `pp.deepTerms` and a raised `pp.maxSteps` close it — which is - why the capture builds on `Emit.ppOpts` rather than its own list. -2. **Invented universe names.** `#check @Decl` instantiates the constant with - fresh universe metavariables and prints them `u_1, u_2, u_3`; the - declaration's `levelParams` were `[w, u, u']`. `ci.type` carries the - declaration's own names, the term does not. -3. **A verification easier than the real check** — a `universe u_1 u_2 u_3` - command above an `example`, supplying by hand the level context - `restateOne` does not have. - -So `--capture` renders, then puts the result through `restateOne` itself — the -same parse, `elabTerm`, `isDefEq` and `withLevelNames` — and returns the string -**only** on `restated`. All three failures produce a rendering that fails that -check, so none can reach `review.yaml` through this path. A capture that cannot -pass the check it exists to feed is not a capture. - -### `C-10` and the bump that invalidates every review at once - -`env_digest` hashes every package rev, so a single dependency bump rotates it -while the mathematics sits still — and `C-10` then reports every human review -as belonging to another environment. This is not a hypothetical. It happened to -the **first review the consuming repository ever recorded**, hours after it was -written: `MathFormalContract` moved `d3df3818 → 21e3b442`, `env_digest` went -`45d9e8ca → 5b2b3d86`, and `C-10` failed while the reviewed statement's digest -was byte-identical on both sides. - -`C-10` was right to fail — the review *was* performed elsewhere — and the wrong -repair is to widen the rule or edit `reviewed_env_digest`, which is the one -thing a review must never suffer silently. - -So `conformance --restate` supplies evidence instead. A review whose -environment moved is carried forward when, and only when, the restate run says -`restated` for its key. `changed` is a finding: the statement moved and the -verdict describes something the declaration no longer says. A key the restate -run does not mention is a finding too, because an omitted entry reads exactly -like a checked one. - -`not_checkable` is a finding **worded as itself**. It is not reported as -`changed`, because the two send a reviewer to different places, and collapsing -them would hide a broken checker behind a pile of apparently-invalidated -reviews. Carried-forward reviews are counted in the rule's reason rather than -passing silently: a reader has to be able to tell a review performed here from -one inherited across a bump. - -### `C-12` and the vacuous pass, one level up - -Every other rule checks what is *present*. A bundle that simply omits its -`build/v1` predicate therefore satisfies all eleven and reports "5 -predicate(s)". `C-12` is the only rule that can see an absence, and -`test_c12_a_bundle_that_simply_omits_its_build_predicate` asserts that no other -rule notices — which is why it exists. - -### What used to be missing, and what still is - -This section previously read "nothing assembles a `bundle.json`, and there is -no `environment.json` or `build.json`, so there is nothing for `conformance` to -run against." Two of those three are now produced: `mfc env` writes the -environment record, and `mfc build` and `mfc seal` write the other two. The -consuming repository's CI produces `environment.json` and `declarations.json` -today, and `test_conformance_passes_over_a_sealed_bundle` runs all twelve rules -over a bundle this package actually wrote rather than one a test assembled. - -What is still absent is stated the same way rather than worked around. -`review.yaml` has no producer and must not have one — it is the axis no machine -may write. `resolution.json` is arXMCP's, and until it exists `C-08` and `C-10` -report `not_run`, which is **not** a pass: the summary line says so on every -run. - -### The fixture tree is built, not checked in - -`C-02` compares a predicate's `sha256` to real bytes, so a checked-in `attest/` -tree would need its digests hand-maintained on every edit. The cost of -generating it is that a generator and a checker sharing a misconception agree -with each other — which is what the mutation tests are for. Each takes the -coherent tree, breaks exactly one link, and requires the matching rule to -notice. - -Building that tree found a real defect in a checked-in fixture. `C-07` -recomputes the environment digest from the environment's own fields, and -`environment-1.0.json` declared a digest computed over **fourteen** packages -while listing **three** — the design note's instance, trimmed for readability, -with the real digest left in place. Rebuilt truthfully from the consuming -repo's `lake-manifest.json`, which also makes `digest.py`'s "nine of the -fourteen packages carry `inputRev` `main` or `master`" checkable against the -fixture instead of only asserted in prose. - -## `seal`: the producer `conformance` was waiting for - -Twelve rules, and until now nothing wrote the file they read. `mfc seal` -assembles `bundle/1.0` — an in-toto Statement v1 with one subject and N -predicates, and deliberately **no** SLSA `verificationResult`, which is exactly -the single collapsed trust token the design forbids. - -### It cannot write the `C-12` fixture - -`C-12` exists because every other rule checks what is *present*: a bundle that -omits its `build/v1` predicate satisfies all eleven others and reports "5 -predicate(s)". A producer willing to write that bundle would be shipping the -rejection fixture as a product, so `seal` refuses when a required predicate -type is missing — and there is no `--force`. The producer and the checker -import `REQUIRED_PREDICATE_TYPES` from the same module, so the two lists cannot -drift. - -### A dirty worktree is refused - -The subject attests a `gitCommit`. If the tree carries uncommitted changes, the -measurements describe bytes that commit does not contain, and every digest in -the bundle becomes a true statement about a tree nobody can fetch. -`--allow-dirty` exists for local experimentation and says on stderr that the -result is explicitly not a release. - -### `self_attested`, said rather than implied - -`true` means the party that wrote the code also produced the measurement. For a -solo-operated repository that is the honest label on `environment`, -`declarations` and `build`, and stating it is worth more than the appearance of -independence. Human review and the corpus resolution are produced elsewhere and -carry `false`. The corpus resolution also carries `env_digest: null` — not a -mismatch and not a match, because it is not produced in a Lean environment at -all. - -## `join`: three axes, three columns, no fourth column - -`conformance` asks whether the artifacts describe the same *build*. `join` asks -whether they describe the same *claims*. A review, a corpus resolution and a -citation each name a statement, and until now nothing checked that the three -ever meet. - -The output is the claim table — one row per `(registry key, declaration)` -binding: - -``` - key decl claimed faithful confirmed resolved frontier - stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2 Topic.thm one_way adequate one_way current - - stmt:9f4c1a20b7d3:bridgeland2007.prop-8.1 Topic.thm exact not_run not_run not_run gltilde-universal-cover -``` - -The second row is what the table exists for: the author claims `exact`, no -reviewer has looked, the corpus was never asked, and a frontier item is open. -No single token can say that, which is why there are separate columns and no -verdict — `test_no_column_is_a_verdict` keeps it that way. Absent evidence -prints `not_run`, so the table has no empty cells to misread. - -Run against this repo's own test emission it reports, correctly: - -``` -0 passed, 0 failed, 6 not_run -8 binding(s) over 8 key(s); 0 reviewed; 0 resolved; 1 with an open frontier -``` - -Nothing here is reviewed or resolved, and the output says so rather than -looking clean. - -### A verdict about another environment is not a weak verdict about this one - -The digest join answers *which statement was reviewed*. It says nothing about -*which environment the reviewer was looking at* — and a review of Lean v4.29 is -no evidence at all about a v4.31 build. That skew is not hypothetical: it is the -standing gap between this repo's pin and the one arXMCP's REPL runs. - -So `join` takes `--environment`, and a review whose `reviewed_env_digest` -disagrees with it renders `not_applicable`: - -``` - key decl claimed faithful confirmed resolved frontier - stmt:9f4c1a20b7d3:bridgeland2007.lem-8.2 Topic.thm exact not_applicable not_applicable not_run - - -1 binding(s) over 1 key(s); 0 reviewed; 0 resolved; 0 with an open frontier; 1 reviewed against another environment -``` - -Three things about that line are deliberate: - -- **It is a rendering, not a finding.** Exit code stays `0`. Being handed a - record built elsewhere is legitimate; the only correct response is to say it - does not apply here. `conformance`'s **C-10 still FAILs** the same document, - and that is not a contradiction — C-10 asks whether the *producer* assembled a - coherent bundle, and one shipping a foreign-env review beside this environment - is incoherent. Producer and consumer are different questions. -- **`not_applicable` is counted on its own**, never folded into `reviewed` (that - would restate the hole as a statistic) and never into the unreviewed remainder - (that would lose the fact that a human has already read these — the cheapest - work in the queue). -- **Without `--environment`, review columns read `not_run`**, and `join` says on - stderr why. Applicability cannot be established, so the axis does not claim it - was. Rendering the verdict instead would reintroduce exactly the silent pass - this section exists to close; the cost of the other direction is an operator - passing one more flag, which is loud and recoverable. - -`not_applicable` is never `pass` and never `fail`. arXMCP's `CLAUDE.md` §4.10 -rule 3 binds the same rule from the other side of the seam. - -### Reviews join by digest, because a name-keyed join fails silently - -`review.decl` records a Lean name. Joining on it breaks under a rename: the -type is unchanged, so `reviewed_statement_digest` still matches while `decl` -dangles — and the join either loses the review (the axis silently reverts to -`not_run`) or, if it is lenient, floats it onto a different declaration. - -So the key is the digest and `decl` is a hint whose disagreement is itself -reported. The two failure modes are kept apart because their remedies differ: - -| what happened | `J-01` says | -|---|---| -| digest matches, name changed | nothing — this is a rename, and it is fine | -| digest misses, `decl` present | the statement was **restated** under the review | -| digest misses, `decl` absent | rename **and** restatement; a human must adjudicate | - -`J-03` refuses to merge disagreeing reviews of one statement. Deduping them -would pick a winner, and the point is that a person has to. - -### `J-06` computes the queue; `--workqueue-out` writes it down - -The work queue — every registry entry with **zero inbound citations**, -partitioned by `kind`, with each entry's open frontier rolled up — is the file -an agent plans against. The rule computes it, and hand it a registry document -and it runs: - -``` - FAIL J-06 the obligation lane: registry entries with no citation - stmt:9f4c1a20b7d3:b: kind='obligation', zero inbound cites; open frontier ['gltilde-universal-cover'] - (conjecture: 1, obligation: 2) -``` - -Counted **per kind and never totalled**. A queue of 90 entries in one lane and -10 in another is not "100 things to do", and a single total is the one number -that makes the file unplannable. - -`mfc join --registry … --workqueue-out attest/workqueue.json` writes that set as -`workqueue/1.0`, the ninth artifact: - -```json -{ - "schema_version": "workqueue/1.0", - "registry_id": "9f4c1a20b7d3", - "registry_sha256": "8c8ec3dd…", - "declarations_sha256": "0cfb36c2…", - "lanes": { - "obligation": { - "count": 1, - "entries": [ - { "key": "stmt:9f4c1a20b7d3:obl-stab-action", - "title": "Show the action is free", - "note": "Owed: no declaration yet asserts freeness…", - "frontier_open": ["gltilde-universal-cover"], - "depends_on": [] } - ] - } - } -} -``` - -**Why this may be written when `conformance` writes nothing.** The rule was -never "no files" — it was "no aggregate verdicts". A queue is an *inventory*: it -records what is owed, judges nothing, and has no axis to collapse. There is no -field it could carry that would make one, and `test_the_queue_is_an_inventory_and_never_a_verdict` -holds it to that. - -**Why it did not have to wait for the size-ceiling decision.** The stated -blocker was that partitioning by `kind` would bake an unmade decision (is there -a zero-axis `sketch` lane?) into a schema. It does not have to: `lanes` is keyed -by whatever kind actually appeared, with `propertyNames` a *pattern* rather than -an enum of the ten `registry/1.0` knows. Adding a member there is a one-schema -MINOR bump, and the two copies cannot disagree because there is only one. -`test_lanes_are_not_a_second_copy_of_the_kind_enum` puts a `sketch` lane through -`mfc validate` today, before the decision exists. - -**No timestamp**, so the file is byte-reproducible from two digested inputs and -`git diff --exit-code attest/` means something. Lanes are sorted, so a lane -appearing or emptying moves one hunk instead of reshuffling the file. - -Refused rather than written empty without `--registry`: a queue with no lanes -and a queue nobody computed are different files, and only one of them means -nothing is owed. - -### The accessor was wrong for three rules at once - -`E-04`, the registry half of `E-05`, and `J-06` all read -`registry["statements"]` as a list of `{key, frontier}`. **No released schema -ever had that shape** — it was invented alongside the rules and then tested -against itself. `registry/1.0` keys `entries` **by citation key**, and -`frontier[]` holds objects whose open state is `discharged_by: null`. - -Two things that hid behind the wrong shape: - -* an entry whose frontier items are **all discharged** has nothing outstanding, - and `E-05` was refusing `relation_claimed: exact` on those. Length was never - the predicate. -* reading an unrecognised document as an *empty* registry makes `E-04` report - every citation in the repository as unknown while `J-06` reports a clean work - queue over zero entries — a finding flood and a vacuous pass out of one bad - input. So `mfc/registry.py` raises, and the callers turn that into `not_run` - with the reason. Same discipline as an unrecognised `.ilean` layout. - -## `check-ilean-coverage`: the only check that looks for what is *absent* - -Every other rule here reads the emission and asks whether what it contains is -allowed. A mis-scoped emitter produces a perfectly valid, perfectly lint-clean -emission over the wrong set of modules, and every downstream artifact is then -immaculate and incomplete. - -`lake build` writes one `.ilean` per module beside the `.olean`, listing the -source-written declaration names. It is plain JSON, and it is produced by Lake -rather than by us — the one description of "what was built" that does not come -from the emitter. - -### Why it is not circular - -The emission carries a `modules[]` array computed by the emitter's own -`inScopeModules`. Comparing `.ilean` files against *that* would check the -emitter against itself: a scope bug drops a module from `modules[]` **and** -from `constants[]`, leaving the emission perfectly self-consistent. So the -in-scope set is re-derived from the filesystem using only the **declared** -`root_lib` (which `--lib` overrides), and `I-04` compares the two derivations. -`test_i04_catches_a_scope_bug_that_a_self_comparison_cannot` is the test that -holds the line. - -### Module prefixes are components, never strings - -`"TopicTest".startswith("Topic")` is `True`, and `TopicTest` is not a submodule -of `Topic`. A string prefix pulls the sibling test library into scope, and then -the coverage check fails on declarations the emitter is *correct* to exclude. -Measured on this repo: 6 built modules, 3 in scope, 29 in-scope declarations, -0 missing — with `MathFormalContractTest` and both executables correctly out. - -### The bootstrap is solved a level up, and that changed what E-08 is for - -Writing this surfaced something about the existing design. #31 warns that a -zero-declaration first build would fire the guard and stop any adopter reaching -a first green build. It cannot: `emission-1.0.schema.json` sets -`constants: minItems 1` and `counts.total/in_scope: minimum 1`, so an empty -emission is **not a representable artifact**, and every subcommand validates -before it reads. - -Which means `E-08`'s counts half — documented above as the vacuous-pass rule — -is **unreachable through any `mfc` subcommand**. The `empty-emission` fixture -is rejected by `mfc validate`, not by `E-08`; its test calls `check()` directly -and so never noticed. That is the *right* arrangement, and the same one -`additionalProperties: false` gives the trust-token ban — a structural -guarantee beats a rule that a caller can skip. But it was credited to the wrong -mechanism, so both are now labelled for what they are, and -`test_an_empty_emission_is_not_a_representable_artifact` pins the schema -constraint so that relaxing it becomes a visible decision rather than a silent -transfer of responsibility to a rule nothing runs. - -The half that no `minItems` can see is the **partial** sweep, and that is what -this command is for. No `--allow-empty` flag exists, deliberately: it would -collapse "genuinely empty repository" and "mis-scoped emitter" into one state, -which is the exact failure the check exists to prevent. They are already -distinct — `.ilean` carrying declarations while `constants[]` is empty is the -bug; both empty is a fresh repo; **no `.ilean` at all is exit 2**, because a -mis-pointed build directory must never be reportable as full coverage. - -## `init`: the measure is a green build on run one - -The test of this command is not that it writes files. It is that the tree it -writes **passes the rest of `mfc` with no hand-editing** — because an adopter -whose first CI run is red learns nothing about their own work, and the most -likely thing they do next is delete the workflow. - -That constraint is sharper than it looks, and it connects directly to the -`minItems: 1` finding above: an emission over zero declarations is not a -representable artifact, so **the scaffold has to ship a real Lean -declaration**. `AnalyticNT/Basic.lean` carries one, with the reason written in -the file so it does not get tidied away. - -`test_the_generated_repository_survives_the_whole_chain` renders a repo, -`lake build`s it, runs its emitter, and then puts the result through `validate`, -`lint`, `check-ilean-coverage`, `bundle` and `join`. Mathlib is swapped for a -local path require, because the question is whether the *generated Lean* -compiles, not whether Lake can download. Measured on the real thing: builds in -14 jobs, emits 1 constant, `lint` 7 passed / 0 failed, coverage 5 passed / 0 -failed. - -That test is the only thing establishing the central claim, so **its skip is -refusable**: with `MFC_REQUIRE_LAKE=1` a missing `lake` is a failure rather than -a skip, and CI sets it in the job that has a toolchain. A skipped check reads -exactly like a passing one in a green run. - -### It renders files and nothing else - -No `git init`, no remote, no commit. A hand-initialised repository has no -remote, no CI permissions, no branch protection and no provisioning, and a tool -that quietly produced one hands you something that looks finished and is not. -`mfc init` prints what it did *not* do, in order, and refuses a non-empty -directory without `--force` — the first thing it would otherwise overwrite is a -`lakefile.toml` somebody wrote. - -Every pin must be 40-hex. A branch is refused because `lake update` re-resolves -it, so the pin would stop pinning with nothing in the repo changing to show it. - -### Rendered with the standard library, not copier — and when to revisit - -The architecture note specifies copier, and its `copier update` is the stated -migration path for a MAJOR schema bump across N topic repos. That is a real -benefit with, today, **no users**: one topic repo exists and it was not created -from a template, so there is nothing for `copier update` to update. Against it, -copier pulls jinja2, pydantic, plumbum and questionary into a package that -argues its own placement decisions from dependency discipline. - -So the templates are plain text with `@@TOKEN@@` substitution — over -`str.format` and `string.Template` because Lean uses both `{}` and `$`, and a -scaffolder that mangles the file it writes is worse than none. A test asserts -no rendered file carries a live token, and the renderer refuses rather than -shipping one. - -**Reversal condition:** adopt copier when a second topic repo exists, *was -created by this command*, and a MAJOR schema bump is due. These files become -the template with the tokens rewritten to `{{ }}`. - -## `registry`: the only hand-authored artifact - -Everything else here is emitted by a program and recomputed by another one. The -registry is typed by a person, at 20–40 minutes an entry, so its rules are -about the mistakes typing makes. - -`registry-1.0.schema.json` was **transcribed** from the design note rather than -authored, the same discipline `digest.py` used — it was given in full there, and -it turned out to be blocked on nothing. The open size-ceiling decision adds an -enum member (a MINOR bump) and a policy; neither moves a shape. - -```bash -mfc registry init # mint a 12-hex id, once per repository -mfc registry validate registry/foo.yaml --frontier-kind-labels mathlib-gap -``` - -The two rules that carry the most weight: - -* **`R-02` recomputes `quote_sha256` from the inline text.** Without it the - digest is a number somebody typed — and `registry_sha256`, the entire - cross-repo freshness mechanism, is built from digests that were never checked - against what they summarize. It is whitespace-insensitive, like the digest - it uses, so a re-wrap does not rotate every citation. -* **`R-06` refuses a key shaped like a corpus id.** A `chunk_id` is exactly what - a corpus hands you, so someone will paste one in — and chunk ids *rotate* on - re-parse with no alias table, so the citation silently stops resolving while - the old id stays addressable. `@[cites]` rejects the shape at compile time - too; both, deliberately, because a hand-edited YAML file never passes through - Lean. - -### Two of the nine were already structural - -The design note tables these as *"rules over the registry that JSON Schema -cannot express."* True of seven. Running the fixtures through the CLI showed it -is **not** true of `R-01` and `R-06`: `source.version` carries -`pattern: ^v[0-9]+$` at the property level, and `entries` carries -`propertyNames: {$ref: citationKey}`. Both fixtures fail `mfc validate` before -`mfc registry validate` reaches the rule. - -Same shape as `E-08`, and the same answer: the structural guarantee is the -stronger arrangement, the rules stay as backstops for a caller that skipped -validation, and `SCHEMA_ENFORCED` in the tests asserts *which layer catches -which* rather than letting a fixture pass the suite while proving nothing. - -### One thing the transcription got wrong, and the fix - -Transcribing the note faithfully preserved a defect the note's own issue (#21) -had already identified: `mint_resolution` was schema-**required** and non-empty -for every kind but `obligation`, so **no entry could be minted until a resolver -existed** — and standing up the resolver is a later migration step. An adopter -with no corpus running could not create their first entry. - -Relaxed as the issue asks, to optional-with-reason: any kind may carry -`mint_resolution: null`, and a null **must** carry `mint_unresolved_reason`. -That is the `not_run` discipline one level down — *nobody asked the corpus* and -*the corpus had no answer* are different facts, and neither may present as -*matched*. Expressible in JSON Schema, so it is structural rather than an -`R` rule, and it has a rejection fixture like everything else. - -Amended in `registry/1.0` rather than minted as `1.1`: the schema landed in the -same session and nothing consumes it yet. - -### The fixtures carry no marker key - -Unlike `artifacts/invalid/`, the registry rejection fixtures have no -`$comment_fixture`. `additionalProperties: false` would reject the marker -rather than the defect, and the fixture would never reach the rule under test — -green suite, nothing proved. The rationale lives in -`testdata/registries/invalid/README.md`, and every fixture is a document that -validates against the schema and fails on exactly one content rule. - -## `bundle` recomputes; it does not carry anything across - -The emission is produced by the topic repo's own emitter in the topic repo's -own build. It is an **input**, not a source of truth. So `axioms` is re-sorted -and re-deduped, `contains_sorry_ax` is recomputed from that list, `counts` are -recounted from `constants[]`, and `axioms_disallowed` is derived from the -environment's `axiom_policy` — a field the emission deliberately does not -report at all, so there is no value to disagree with. - -This is not suspicion of the emitter. It is that a producer reporting its own -verdict has one failure mode no amount of care removes, and the contract exists -to keep that failure mode out. There is no code path here that emits a clean -`axioms_disallowed` for a declaration whose axioms contain `sorryAx`. - -Both inputs are validated **before** anything is derived from them, and the -output is validated **before** it is written — `mfc` must not be able to emit -an artifact its own schema rejects. - -## Digests are pinned by data, not by agreement with ourselves - -`digest.py` is frozen: any change is a MAJOR bump on every artifact carrying a -digest. `tests/test_digest.py` reproduces the three values the design note -recorded as `[COMPUTED]` against the real repository at `f166a3d` — the -`env_digest` and both statement digests — so a refactor that changes key order, -separators, or the NFC-then-collapse order fails immediately. - -That matters more here than usual. The fixture corpus lives inside one of the -implementations it referees, so "our code agrees with our code" proves nothing; -agreement with values computed before this code existed does. It is red-team -gap 16's mitigation. - -The properties those digests encode, each with its own test: - -* a **def's body is part of its statement** — two defs with one type and - different bodies are different claims; -* a **theorem's proof is not** — folding it in would make every proof edit read - as a statement change, destroying the signal review depends on; -* a **rename does not rotate** anything — citations anchor to a registry key; -* **re-wrapping does not rotate** anything — `type_pp` carries hard line breaks - at the pinned `format.width`. - -## `validate`, and why it does not take a `--schema` - -Every artifact carries `schema_version` as its first key, and `validate` reads -it rather than accepting a flag. That makes the artifact's **self-description** -part of what is checked: a file called `build.json` that declares -`emission/1.0` is validated as an emission and fails, instead of being quietly -checked as a build. `--schema` exists only to override for debugging, and -needing it means something is already wrong. - -A `schema_version` this build does not carry is a **hard failure**, never a -skip. Skipping would let an artifact from a future contract version pass -unchecked, which is exactly the tolerant mode the design forbids. - -All errors are reported, not the first. For a cross-field `allOf` the first -error is often the least informative one, and a validator that stops early -turns fixing an artifact into N round trips. - -```bash -python3 -m pytest contract/tests -q -``` - -Exit codes are the contract with CI and are fixed: `0` clean, `1` findings, -`2` usage or environment error. The gap between 1 and 2 is load-bearing — a job -that reads "the linter crashed" as "the linter passed" is the vacuous pass this -project exists to prevent, which is why an empty or mis-pointed `--schema-dir` -is an error rather than a silent success. - -There is no `pyproject.toml` yet. `mfc` is invoked as a module. ADR-0009 makes -it a *shared* tool, so it will need to be installable before the consuming repo -can use it; that is a follow-up, not an oversight. - -## `lint-schemas`, and why the traversal is deep - -arXMCP's `CLAUDE.md` §4.9 forbids any single token that collapses distinct -trust questions. A schema declaring a property named `status` or `verified` -hands a producer that token back, so declaring one fails the build. - -The design note specifies this as "walking every `properties` key of every -schema". That reading is inadequate against the first schema it would be run -on: `emission/1.0` declares `constant` and `cite` under `$defs`, so a top-level -`doc["properties"]` walk never sees `relation_claimed`, `axioms`, `type_pp` or -anything else that matters. The walk therefore recurses through `$defs`, -`allOf`/`anyOf`/`oneOf`, `items`, `patternProperties`, `if`/`then`/`else` and -the rest. `$ref` is deliberately not followed — it points at a definition the -walk already visits, and following it would double-report and can cycle. - -`testdata/schemas/invalid/nested-verdict.schema.json` exists to hold that line: -every forbidden name in it is buried where the naive walk cannot see it, and a -test asserts the naive walk finds **nothing** in it. If that test ever starts -passing for the wrong reason, the fixture has stopped testing depth. - -**The banned set is 13 names, not 6.** The design note's literal -`FORBIDDEN_PROPERTY_NAMES` is 13; issues #19 and #21 quote 6. The 13-name set -is a strict superset and is the literal artifact specified, so it is what -ships. The discrepancy is recorded rather than silently resolved, because this -list *is* the rule being mechanised. diff --git a/contract/mfc.egg-info/SOURCES.txt b/contract/mfc.egg-info/SOURCES.txt deleted file mode 100644 index ad7da6a..0000000 --- a/contract/mfc.egg-info/SOURCES.txt +++ /dev/null @@ -1,106 +0,0 @@ -README.md -pyproject.toml -./mfc/__init__.py -./mfc/bootstrap.py -./mfc/build.py -./mfc/bundle.py -./mfc/cli.py -./mfc/conformance.py -./mfc/containment.py -./mfc/digest.py -./mfc/env.py -./mfc/freshness.py -./mfc/ilean.py -./mfc/join.py -./mfc/lint.py -./mfc/registry.py -./mfc/restate.py -./mfc/review.py -./mfc/rules.py -./mfc/rules_registry.py -./mfc/scaffold.py -./mfc/seal.py -./mfc/validate.py -./mfc/withdrawals.py -./mfc/schema/build-1.0.schema.json -./mfc/schema/bundle-1.0.schema.json -./mfc/schema/declarations-1.0.schema.json -./mfc/schema/emission-1.0.schema.json -./mfc/schema/environment-1.0.schema.json -./mfc/schema/registry-1.0.schema.json -./mfc/schema/resolution-1.0.schema.json -./mfc/schema/restate-1.0.schema.json -./mfc/schema/review-1.0.schema.json -./mfc/schema/run-1.0.schema.json -./mfc/schema/withdrawals-1.0.schema.json -./mfc/schema/workqueue-1.0.schema.json -mfc/__init__.py -mfc/bootstrap.py -mfc/build.py -mfc/bundle.py -mfc/cli.py -mfc/conformance.py -mfc/containment.py -mfc/digest.py -mfc/env.py -mfc/freshness.py -mfc/ilean.py -mfc/join.py -mfc/lint.py -mfc/registry.py -mfc/restate.py -mfc/review.py -mfc/rules.py -mfc/rules_registry.py -mfc/scaffold.py -mfc/seal.py -mfc/validate.py -mfc/withdrawals.py -mfc.egg-info/PKG-INFO -mfc.egg-info/SOURCES.txt -mfc.egg-info/dependency_links.txt -mfc.egg-info/entry_points.txt -mfc.egg-info/requires.txt -mfc.egg-info/top_level.txt -mfc/schema/build-1.0.schema.json -mfc/schema/bundle-1.0.schema.json -mfc/schema/declarations-1.0.schema.json -mfc/schema/emission-1.0.schema.json -mfc/schema/environment-1.0.schema.json -mfc/schema/registry-1.0.schema.json -mfc/schema/resolution-1.0.schema.json -mfc/schema/restate-1.0.schema.json -mfc/schema/review-1.0.schema.json -mfc/schema/run-1.0.schema.json -mfc/schema/withdrawals-1.0.schema.json -mfc/schema/workqueue-1.0.schema.json -tests/test_allowlist.py -tests/test_bootstrap.py -tests/test_build.py -tests/test_bundle.py -tests/test_conformance.py -tests/test_containment.py -tests/test_digest.py -tests/test_digest_corpus.py -tests/test_discharges.py -tests/test_env.py -tests/test_external.py -tests/test_freshness.py -tests/test_ilean.py -tests/test_join.py -tests/test_lint_schemas.py -tests/test_multiroot.py -tests/test_quote_mode.py -tests/test_referent.py -tests/test_registry.py -tests/test_restate.py -tests/test_review.py -tests/test_rules.py -tests/test_rules_registry.py -tests/test_scaffold.py -tests/test_schemas.py -tests/test_seal.py -tests/test_validate.py -tests/test_vocabulary.py -tests/test_volatile.py -tests/test_withdrawals.py \ No newline at end of file diff --git a/contract/mfc.egg-info/dependency_links.txt b/contract/mfc.egg-info/dependency_links.txt deleted file mode 100644 index 8b13789..0000000 --- a/contract/mfc.egg-info/dependency_links.txt +++ /dev/null @@ -1 +0,0 @@ - diff --git a/contract/mfc.egg-info/entry_points.txt b/contract/mfc.egg-info/entry_points.txt deleted file mode 100644 index 5e29550..0000000 --- a/contract/mfc.egg-info/entry_points.txt +++ /dev/null @@ -1,2 +0,0 @@ -[console_scripts] -mfc = mfc.cli:main diff --git a/contract/mfc.egg-info/requires.txt b/contract/mfc.egg-info/requires.txt deleted file mode 100644 index 860d28e..0000000 --- a/contract/mfc.egg-info/requires.txt +++ /dev/null @@ -1,7 +0,0 @@ -jsonschema>=4.18 - -[test] -pytest>=7 - -[yaml] -PyYAML>=6 diff --git a/contract/mfc.egg-info/top_level.txt b/contract/mfc.egg-info/top_level.txt deleted file mode 100644 index 26b94e1..0000000 --- a/contract/mfc.egg-info/top_level.txt +++ /dev/null @@ -1 +0,0 @@ -mfc