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/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 deleted file mode 100644 index 9848c3e..0000000 --- a/contract/mfc.egg-info/PKG-INFO +++ /dev/null @@ -1,176 +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.9 -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 seven** artifact formats | -| `mfc/lint.py` | the banned-property lint | -| `mfc/validate.py` | artifact validation | -| `mfc/cli.py` | `mfc lint-schemas`, `mfc validate` | -| `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/artifacts/invalid/` | artifacts that must fail a cross-field rule | -| `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. - -### 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. - -## `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 186a222..0000000 --- a/contract/mfc.egg-info/SOURCES.txt +++ /dev/null @@ -1,33 +0,0 @@ -README.md -pyproject.toml -./mfc/__init__.py -./mfc/cli.py -./mfc/lint.py -./mfc/validate.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/resolution-1.0.schema.json -./mfc/schema/review-1.0.schema.json -mfc/__init__.py -mfc/cli.py -mfc/lint.py -mfc/validate.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/resolution-1.0.schema.json -mfc/schema/review-1.0.schema.json -tests/test_lint_schemas.py -tests/test_schemas.py -tests/test_validate.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 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..8f71cef 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": [ @@ -244,7 +252,34 @@ } }, { - "$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": "`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. `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": { @@ -261,7 +296,8 @@ "enum": [ "current", "drifted", - "unresolvable" + "unresolvable", + "not_applicable" ] }, "similarity": { 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..52b2515 100644 --- a/contract/testdata/artifacts/valid/resolution-1.0.json +++ b/contract/testdata/artifacts/valid/resolution-1.0.json @@ -40,6 +40,28 @@ "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." + }, + { + "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": { @@ -47,6 +69,7 @@ "drifted": 0, "unresolvable": 0, "paper_absent": 0, - "not_run": 1 + "not_run": 1, + "not_applicable": 2 } } 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_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." + ) 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.