diff --git a/.github/workflows/formal-maintenance.yml b/.github/workflows/formal-maintenance.yml new file mode 100644 index 00000000..8641d6e3 --- /dev/null +++ b/.github/workflows/formal-maintenance.yml @@ -0,0 +1,72 @@ +name: Formal maintenance + +on: + workflow_dispatch: + schedule: + - cron: "17 8 * * 1" + push: + branches: [main] + paths: + - ".github/workflows/formal-maintenance.yml" + - "lean-toolchain" + - "lakefile.toml" + - "lake-manifest.json" + - "formal/**" + - "tools/check_lean_specs.py" + - "tools/check_logic_fixtures.py" + - "baseline/**/*.py" + - "datasets/**/*.py" + - "decomposer/**/*.py" + - "search/**/*.py" + - "training/**/*.py" + - "utils/**/*.py" + - "verifier/**/*.py" + pull_request: + paths: + - ".github/workflows/formal-maintenance.yml" + - "lean-toolchain" + - "lakefile.toml" + - "lake-manifest.json" + - "formal/**" + - "tools/check_lean_specs.py" + - "tools/check_logic_fixtures.py" + - "baseline/**/*.py" + - "datasets/**/*.py" + - "decomposer/**/*.py" + - "search/**/*.py" + - "training/**/*.py" + - "utils/**/*.py" + - "verifier/**/*.py" + +permissions: + contents: read + +concurrency: + group: formal-maintenance-${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + maintain: + name: Lean 4.32 proof and conformance gate + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout code + uses: actions/checkout@v6 + + - name: Install pinned Lean toolchain + uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + test: false + lint: false + + - name: Build without warnings + run: lake build --wfail + + - name: Check theorem links, tests, dependencies, and axiom footprints + run: python3 tools/check_lean_specs.py + + - name: Replay shared logical evaluation fixtures + run: python3 tools/check_logic_fixtures.py diff --git a/.github/workflows/pytest.yml b/.github/workflows/pytest.yml index 88c3199c..660d238c 100644 --- a/.github/workflows/pytest.yml +++ b/.github/workflows/pytest.yml @@ -17,6 +17,12 @@ on: - "verifier/**" - "baseline/**" - "training/**" + - "formal/**" + - "tools/check_lean_specs.py" + - "tools/check_logic_fixtures.py" + - "lakefile.toml" + - "lake-manifest.json" + - "lean-toolchain" pull_request: paths: - ".github/workflows/pytest.yml" @@ -30,6 +36,12 @@ on: - "verifier/**" - "baseline/**" - "training/**" + - "formal/**" + - "tools/check_lean_specs.py" + - "tools/check_logic_fixtures.py" + - "lakefile.toml" + - "lake-manifest.json" + - "lean-toolchain" jobs: test: diff --git a/.gitignore b/.gitignore index 83972fad..0ec5c62d 100644 --- a/.gitignore +++ b/.gitignore @@ -205,6 +205,7 @@ tempCodeRunnerFile.py # Ruff stuff: .ruff_cache/ +.lake/ # PyPI configuration file .pypirc diff --git a/FORMAL_LOGIC.md b/FORMAL_LOGIC.md new file mode 100644 index 00000000..8f71926d --- /dev/null +++ b/FORMAL_LOGIC.md @@ -0,0 +1,305 @@ +# Maintaining AMFV's formal logic + +AMFV uses Lean to specify and test structural rules at boundaries where an +ordinary program can return plausible-looking but invalid data. The current +models cover source URL admission, scraper accounting, verification receipts, +cache admission, and evaluation success. + +This is an engineering layer, not a claim that AMFV is wholly verified. Lean +proves properties of the finite models in `formal/`. Python tests and shared +fixtures connect those models to runtime behavior. + +## Why this layer exists + +Medical fact verification depends on more than a model's final score. The +system must also preserve where evidence came from, which evidence a receipt +uses, whether cached work belongs to the same scope, and whether an evaluation +actually agrees with its reference. + +These rules are: + +- small enough to state precisely; +- important enough that silent failure is expensive; +- stable enough to serve as interfaces between components; and +- easy to under-test if only happy paths are exercised. + +Lean gives these rules an executable, reviewable definition. It is a +development and CI dependency only; AMFV's Python runtime does not invoke Lean. + +## What is and is not proved + +The Lean library proves the named theorems about the types and functions +declared under `formal/`. The repository then checks that selected Python +symbols point to real theorems and have paired runtime tests. + +This establishes a maintained correspondence. It does not prove: + +- arbitrary Python bytecode correct; +- arbitrary HTML or JSON correctly parsed; +- a medical claim true or false; +- evidence clinically sufficient; +- a source corpus complete; or +- the network, clock, or upstream source trustworthy. + +When adding a theorem, state its assumptions in its types or surrounding +documentation. Do not describe a model property as a property of the whole +application unless the runtime bridge actually enforces it. + +## Repository layout + +| Path | Responsibility | +| --- | --- | +| `lean-toolchain` | Pins the exact Lean release used locally and in CI. | +| `lakefile.toml` | Declares the `AMFV` library and `amfv_logic` executable. | +| `lake-manifest.json` | Records the dependency-free Lake project state. | +| `formal/AMFV.lean` | Imports the public formal library. | +| `formal/AMFV/Logic/` | General adversarial logical gates. | +| `formal/AMFV/Scraping/` | URL policy and scraper-accounting models. | +| `formal/AMFV/Verification/` | Receipt, cache, verdict, and evaluation models. | +| `formal/AMFV/LogicalEval.lean` | JSONL logical-evaluation executable. | +| `formal/AMFV/ProofBoundary.lean` | Explicit statements about the proof boundary. | +| `formal/fixtures/logical-eval.jsonl` | Shared Lean/Python conformance cases. | +| `tools/check_lean_specs.py` | Proof hygiene, dependency, tag, test, and axiom checks. | +| `tools/check_logic_fixtures.py` | Replays shared fixtures through Lean. | +| `.github/workflows/formal-maintenance.yml` | Pull-request, push, scheduled, and manual gate. | + +The formal project intentionally uses only Lean's standard library. Keeping the +model small and dependency-free makes it easier for maintainers to audit and +keeps CI failures attributable to this repository. + +## Local setup + +Install Lean through `elan`, Lean's toolchain manager. From the repository root, +confirm that the pinned version is selected: + +```sh +lean --version +lake --version +cat lean-toolchain +``` + +`elan` reads `lean-toolchain` automatically. The expected pin is +`leanprover/lean4:v4.32.0`. + +Install the Python development environment separately: + +```sh +uv sync --dev +``` + +No Lean package installation is required. A successful first build downloads +or selects the pinned toolchain and builds the local project: + +```sh +lake build --wfail +``` + +## The normal maintenance loop + +Use the same counterexample from discovery through proof and runtime repair: + +1. Identify a structural state that AMFV must reject or account for. +2. Reduce it to the smallest finite model that preserves the failure. +3. Add the counterexample to Lean and show why the old gate is insufficient. +4. State and prove a narrow invariant for the repaired gate. +5. Patch the Python boundary that enforces the rule. +6. Add a focused Python regression test using the same counterexample. +7. Link the runtime symbol and test to the theorem. +8. Add or update shared JSONL fixtures when the rule is part of the logical + evaluator protocol. +9. Run the full maintenance gate before requesting review. + +Prefer a theorem about one admission or accounting decision over a theorem that +recreates an entire Python subsystem. Small models are easier to review, reuse, +and keep aligned. + +## Linking Python to a theorem + +Put a `lean-spec` comment immediately above the supported Python function or +class: + +```python +# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority +def is_allowed_chapter(...): + ... +``` + +Put the matching `lean-spec-test` comment immediately above a pytest test: + +```python +# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority +def test_rejects_off_domain_chapter(...): + ... +``` + +The fully qualified name must resolve to a Lean `theorem`, not merely a +definition. Every runtime tag must have at least one paired test tag. + +`tools/check_lean_specs.py` enforces that: + +- both annotations are attached directly to Python declarations; +- each runtime annotation has a paired runtime test; +- every named declaration exists and is a theorem; +- tagged theorems have an empty axiom footprint; +- Lean sources contain no `sorry`, `admit`, `axiom`, `constant`, or `opaque` + proof escape; and +- `lake-manifest.json` contains no external packages. + +If a Python symbol implements several independent rules, use a small validating +function for each rule instead of making one annotation stand for an ambiguous +bundle of behavior. + +## Shared logical-evaluation fixtures + +`lake exe amfv_logic` accepts one `amfv.logic.v1` JSON object per line and emits +one result per line. Supported input kinds are: + +- `verifier_receipt`; +- `cache_admission`; and +- `evaluation_case`. + +Each fixture in `formal/fixtures/logical-eval.jsonl` includes +`expected_valid` and `expected_violations`. Violation codes are part of the +developer-facing protocol: keep them stable unless a deliberate protocol change +is documented and applied to both implementations. + +When extending the protocol: + +1. define the rule and violation code in the Lean model; +2. update `formal/AMFV/LogicalEval.lean`; +3. update the Python mirror; +4. add valid, invalid, boundary, and malformed fixtures; +5. make both implementations return the same ordered result; and +6. run both the Lean fixture replay and Python conformance tests. + +Fixtures should include the smallest counterexample, not just realistic large +objects. For time rules, cover exact boundaries, unreasonable values, UTC +normalization, and daylight-saving folds where applicable. For collections, +cover missing fields, wrong shapes, unknown identifiers, duplicates, overlaps, +and empty directional evidence. + +## Required checks + +Run these commands from the repository root: + +```sh +lake build --wfail +python3 tools/check_lean_specs.py +python3 tools/check_logic_fixtures.py +uv run pytest +uv run ruff check . +uv run ruff format --check . +``` + +When changing a package's public or packaging surface, also build that package, +for example: + +```sh +uv build --package amfv-verifier +``` + +`--wfail` is intentional: new Lean warnings are maintenance failures rather +than deferred cleanup. + +## Continuous maintenance + +`.github/workflows/formal-maintenance.yml` runs when formal files, proof-link +tools, the workflow itself, or Python component files change. It also runs every +Monday and can be started manually with `workflow_dispatch`. + +The workflow: + +1. checks out the repository; +2. installs the version from `lean-toolchain`; +3. builds Lean with warnings treated as errors; +4. verifies theorem links, paired tests, dependencies, and axiom footprints; +5. replays the shared logical-evaluation fixtures. + +The scheduled run is a drift detector. Do not solve a scheduled failure by +loosening a theorem, deleting a counterexample, or weakening the checker. First +identify whether the toolchain, model, runtime link, or fixture protocol drifted. + +## Updating Lean + +Treat a Lean upgrade as its own pull request: + +1. change `lean-toolchain` to the intended exact release; +2. run `lake update` to refresh `lake-manifest.json`; +3. run every required check above; +4. inspect warnings and proof changes rather than applying broad mechanical + rewrites; +5. confirm `packages` remains empty in `lake-manifest.json`; +6. record meaningful language or behavior changes in the pull-request body. + +Do not use an unpinned channel such as `stable` or `nightly`. Do not add Mathlib +or another Lean dependency merely to shorten a small proof; propose that change +explicitly with its maintenance and supply-chain cost. + +## Diagnosing failures + +### A `lean-spec` target does not resolve + +Import its module from `formal/AMFV.lean`, check the fully qualified namespace, +and run: + +```sh +lake env lean formal/AMFV.lean +python3 tools/check_lean_specs.py +``` + +### A theorem has an axiom dependency + +Inspect it directly: + +```lean +#print axioms AMFV.Namespace.theorem_name +``` + +Remove the assumption or proof escape. Do not suppress the checker. + +### Lean and Python disagree on a fixture + +Reduce the failing record to the smallest JSON object that still disagrees. +Then compare: + +```sh +lake exe amfv_logic < formal/fixtures/logical-eval.jsonl +python3 tools/check_logic_fixtures.py +uv run pytest +``` + +Determine whether the model, Python mirror, or expected protocol result is +wrong. The formal implementation is not automatically authoritative about +medical meaning; the intended rule must be reviewed. + +### CI passes locally but fails on the schedule + +Confirm the checked-in toolchain and manifest match the local environment, then +rerun with a clean Lake build directory if necessary. If the failure is caused +by an upstream action change, pin or repair the workflow in a focused pull +request rather than bypassing the formal gate. + +## Review checklist + +Before merging a formal-logic change, verify: + +- [ ] The motivating bad state is concrete and reproducible. +- [ ] The model is smaller than the runtime behavior it constrains. +- [ ] Assumptions and proof boundaries are explicit. +- [ ] The theorem has no proof placeholders or axiom dependencies. +- [ ] The Python enforcement point has a `lean-spec` tag. +- [ ] A focused regression test has the matching `lean-spec-test` tag. +- [ ] Shared fixtures cover both acceptance and rejection when applicable. +- [ ] Violation codes and protocol changes are deliberate and documented. +- [ ] Lean remains a development/CI dependency, not a runtime dependency. +- [ ] All required local and CI checks pass. + +## Choosing the next proof target + +Good targets are deterministic admission, accounting, freshness, scope, and +agreement rules whose failure can silently contaminate later stages. Avoid +using Lean to restate broad product intent or to make claims about clinical +truth that require empirical evidence. + +The practical question is: **what invalid state could still look valid to the +next component?** Start there. diff --git a/README.md b/README.md index 8721bae3..9767ef11 100644 --- a/README.md +++ b/README.md @@ -26,3 +26,24 @@ Following Baichuan-M3, the task is split into three models across four steps: | [`training`](training/README.md) | Training experiments and recipes for the above | Independent | The **Workspace** column marks membership in the root `uv` workspace. Independent packages (`baseline`, `training`) are excluded so they can evolve on their own. + +## Formal logical evaluation + +AMFV uses a dependency-free Lean 4.32.0 library to model structural invariants +at high-risk boundaries such as source URL admission, scraper accounting, +verification receipts, cache freshness, and evaluation success. + +```sh +lake build --wfail +python3 tools/check_lean_specs.py +python3 tools/check_logic_fixtures.py +``` + +Python functions annotated with `# lean-spec:` are backed by a named theorem +and an adversarial runtime test. This establishes conformance to the modeled +invariant; it does not claim that Lean verifies Python bytecode, arbitrary HTML, +medical truth, or corpus completeness. + +See [`FORMAL_LOGIC.md`](FORMAL_LOGIC.md) for the complete developer and +maintenance guide. The shorter [`formal/README.md`](formal/README.md) is a +directory-level quick reference. diff --git a/datasets/amfv_datasets/scraping/__init__.py b/datasets/amfv_datasets/scraping/__init__.py index cd7cdb06..f3631f9d 100644 --- a/datasets/amfv_datasets/scraping/__init__.py +++ b/datasets/amfv_datasets/scraping/__init__.py @@ -20,7 +20,9 @@ from amfv_datasets.scraping.nice import ( GuidanceListingPage, GuidanceRef, + GuidelineExtractionReceipt, NiceFetchError, + OmittedSection, build_guideline_text, guidance_ref_from_url, list_published_guidance, @@ -30,9 +32,11 @@ __all__ = [ "GuidanceRef", + "GuidelineExtractionReceipt", "GuidanceListingPage", "LinkMode", "NiceFetchError", + "OmittedSection", "OutputFormat", "ScrapeError", "ScrapeRun", diff --git a/datasets/amfv_datasets/scraping/html.py b/datasets/amfv_datasets/scraping/html.py index 2bd1c968..272c8948 100644 --- a/datasets/amfv_datasets/scraping/html.py +++ b/datasets/amfv_datasets/scraping/html.py @@ -3,9 +3,9 @@ from __future__ import annotations import re -from collections.abc import Iterable +from collections.abc import Collection, Iterable from enum import StrEnum -from urllib.parse import urljoin +from urllib.parse import urljoin, urlsplit, urlunsplit from lxml import html as lxml_html from markdownify import MarkdownConverter @@ -40,17 +40,46 @@ def clean_text(value: str, *, drop_numeric_citations: bool = True) -> str: return _WHITESPACE_RE.sub(" ", text).strip() -def absolute_unique_urls(urls: Iterable[str], *, base_url: str) -> list[str]: +def absolute_unique_urls( + urls: Iterable[str], + *, + base_url: str, + allowed_schemes: Collection[str] = ("http", "https"), + allowed_hosts: Collection[str] | None = None, +) -> list[str]: """Normalize URLs against a base URL and remove duplicates. Args: urls: Raw URL values to normalize. base_url: Base URL used for relative links. + allowed_schemes: URL schemes that may be returned. + allowed_hosts: Optional exact hostname allowlist. When set, URLs with + credentials or non-default ports are rejected. """ + normalized_schemes = {scheme.lower() for scheme in allowed_schemes} + normalized_hosts = {host.lower() for host in allowed_hosts} if allowed_hosts is not None else None seen: set[str] = set() normalized_urls: list[str] = [] for raw_url in urls: - url = urljoin(base_url, raw_url).split("#")[0].split("?")[0] + parsed = urlsplit(urljoin(base_url, raw_url)) + scheme = parsed.scheme.lower() + if scheme not in normalized_schemes: + continue + try: + port = parsed.port + except ValueError: + continue + if normalized_hosts is not None: + default_port = 80 if scheme == "http" else 443 if scheme == "https" else None + if ( + parsed.hostname is None + or parsed.hostname.lower() not in normalized_hosts + or parsed.username is not None + or parsed.password is not None + or port not in {None, default_port} + ): + continue + url = urlunsplit(parsed._replace(query="", fragment="")) if url in seen: continue seen.add(url) @@ -58,19 +87,35 @@ def absolute_unique_urls(urls: Iterable[str], *, base_url: str) -> list[str]: return normalized_urls -def first_matching_urls(html_text: str, *, xpaths: Iterable[str], base_url: str) -> list[str]: +def first_matching_urls( + html_text: str, + *, + xpaths: Iterable[str], + base_url: str, + allowed_schemes: Collection[str] = ("http", "https"), + allowed_hosts: Collection[str] | None = None, +) -> list[str]: """Return normalized URLs from the first XPath with matches. Args: html_text: HTML page text to parse. xpaths: XPath expressions that return URL strings. base_url: Base URL used for relative links. + allowed_schemes: URL schemes that may be returned. + allowed_hosts: Optional exact hostname allowlist. """ doc = lxml_html.fromstring(html_text) for xpath in xpaths: urls = doc.xpath(xpath) if urls: - return absolute_unique_urls(urls, base_url=base_url) + normalized_urls = absolute_unique_urls( + urls, + base_url=base_url, + allowed_schemes=allowed_schemes, + allowed_hosts=allowed_hosts, + ) + if normalized_urls: + return normalized_urls return [] diff --git a/datasets/amfv_datasets/scraping/nice.py b/datasets/amfv_datasets/scraping/nice.py index 79d5bb69..b9c92851 100644 --- a/datasets/amfv_datasets/scraping/nice.py +++ b/datasets/amfv_datasets/scraping/nice.py @@ -38,7 +38,7 @@ default_client, scrape_listing_documents, ) -from amfv_datasets.scraping.html import LinkMode, document_title, first_matching_urls, html_to_markdown +from amfv_datasets.scraping.html import LinkMode, absolute_unique_urls, document_title, html_to_markdown from amfv_datasets.scraping.nextjs import script_json_by_id BASE_URL = "https://www.nice.org.uk" @@ -75,6 +75,7 @@ ) _NUMBERED_HEADING_RE = re.compile(r"^\s*\d+(?:\.\d+)*\s+") _SKIP_CHAPTER_SUFFIXES = ("finding-more-information-and-committee-details",) +_NICE_HOSTS = ("nice.org.uk", "www.nice.org.uk") class _NiceScrapeStrategy(StrEnum): @@ -99,12 +100,48 @@ class GuidanceRef: @dataclass(frozen=True) class GuidanceListingPage: - """A NICE published-guidance listing page.""" + """A NICE published-guidance listing page. + + `total` is NICE's source-reported count before AMFV filters unsupported + guidance types. It is not an exact count of eligible or emitted documents. + """ refs: list[GuidanceRef] total: int | None +@dataclass(frozen=True) +class OmittedSection: + """A discovered source section intentionally omitted from the document.""" + + url: str + reason: str + + +@dataclass(frozen=True) +class GuidelineExtractionReceipt: + """Auditable result of extracting overview/chapter source sections.""" + + content: str + section_count: int + title: str + discovered_count: int + retained_urls: tuple[str, ...] + omitted_sections: tuple[OmittedSection, ...] + transformations: tuple[str, ...] + + # lean-spec: AMFV.Scraping.ExtractionReceipt.accounted_receipt_matches_disposition_count + def is_accounted(self) -> bool: + """Return whether disposition cardinalities match the discovered count.""" + return self.discovered_count == len(self.retained_urls) + len(self.omitted_sections) + + +@dataclass(frozen=True) +class _ChapterLinkDiscovery: + accepted: tuple[str, ...] + rejected: tuple[OmittedSection, ...] + + def _listing_url(*, page: int) -> str: return f"{BASE_URL}/guidance/published?sp=on&pa={page}" @@ -149,20 +186,12 @@ def _parse_listing(html_text: str) -> GuidanceListingPage: logger.debug("Skipping unsupported NICE guidance type %s for %s", prefix, ref) continue slug = ref.lower() - path = doc.get("pathAndQuery") or _page_path(ref=ref, slug=slug) - page_url = ( - _page_url(ref=ref, slug=slug) - if prefix in _ADVICE_PREFIXES - else f"{BASE_URL}{path}" - if path.startswith("/") - else path - ) refs.append( GuidanceRef( ref=ref, slug=slug, title=(doc.get("title") or ref).strip(), - page_url=page_url, + page_url=_page_url(ref=ref, slug=slug), ) ) total = results.get("resultCount") @@ -181,14 +210,38 @@ def list_published_guidance(client: httpx.Client, page: int = 1) -> GuidanceList return _parse_listing(response.text) -def _chapter_links(html_text: str, slug: str) -> list[str]: - """Return absolute chapter URLs from a guidance overview table of contents.""" +# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_respects_source_boundary +def _chapter_links(html_text: str, slug: str) -> _ChapterLinkDiscovery: + """Return accepted and rejected chapter URLs from a table of contents.""" chapter_path_match = f"contains(@href, '/guidance/{slug}/chapter/') or contains(@href, '/advice/{slug}/chapter/')" nav_xpaths = ( f"//*[contains(concat(' ', normalize-space(@class), ' '), ' stacked-nav ')]//a[{chapter_path_match}]/@href", f"//ul[contains(concat(' ', normalize-space(@class), ' '), ' nav-list ')]//li//a[{chapter_path_match}]/@href", ) - return first_matching_urls(html_text, xpaths=nav_xpaths, base_url=BASE_URL) + doc = lxml_html.fromstring(html_text) + rejected: list[OmittedSection] = [] + for xpath in nav_xpaths: + raw_urls = doc.xpath(xpath) + if not raw_urls: + continue + authority_accepted = absolute_unique_urls(raw_urls, base_url=BASE_URL, allowed_hosts=_NICE_HOSTS) + accepted = [url for url in authority_accepted if _is_scoped_chapter_url(url, slug)] + for raw_url in raw_urls: + normalized = absolute_unique_urls([raw_url], base_url=BASE_URL, allowed_hosts=_NICE_HOSTS) + if normalized and _is_scoped_chapter_url(normalized[0], slug): + continue + normalized_rejection = absolute_unique_urls([raw_url], base_url=BASE_URL) + rejected_url = normalized_rejection[0] if normalized_rejection else raw_url + reason = "out_of_scope_url" if normalized else "unsafe_url" + rejected.append(OmittedSection(url=rejected_url, reason=reason)) + if accepted: + return _ChapterLinkDiscovery(accepted=tuple(accepted), rejected=tuple(dict.fromkeys(rejected))) + return _ChapterLinkDiscovery(accepted=(), rejected=tuple(dict.fromkeys(rejected))) + + +def _is_scoped_chapter_url(url: str, slug: str) -> bool: + path = urlparse(url).path.lower() + return path.startswith(f"/guidance/{slug}/chapter/") or path.startswith(f"/advice/{slug}/chapter/") def _overview_markdown(html_text: str, *, ref: GuidanceRef, link_mode: LinkMode) -> str: @@ -283,7 +336,19 @@ def build_guideline_text( link_mode: Whether links are kept as markdown links or stripped to their visible text (default: LinkMode.KEEP). """ - overview = client.get(ref.page_url) + receipt = _build_guideline_receipt(client, ref, link_mode=link_mode) + return receipt.content, receipt.section_count, receipt.title + + +def _build_guideline_receipt( + client: httpx.Client, + ref: GuidanceRef, + *, + link_mode: LinkMode = LinkMode.KEEP, +) -> GuidelineExtractionReceipt: + """Scrape a guideline and account for retained and omitted sections.""" + page_url = _validated_page_url(ref) + overview = client.get(page_url) overview.raise_for_status() title = ( ref.title @@ -294,28 +359,61 @@ def build_guideline_text( suffixes=(" | Guidance | NICE", " | Advice | NICE"), ) ) - chapter_urls = _chapter_links(overview.text, ref.slug) - if not chapter_urls: + chapter_links = _chapter_links(overview.text, ref.slug) + if not chapter_links.accepted: raise NiceFetchError(f"No chapters found for guidance '{ref.ref}'") sections: list[str] = [] + retained_urls: list[str] = [] + omitted_sections = list(chapter_links.rejected) overview_markdown = _overview_markdown(overview.text, ref=ref, link_mode=link_mode) if overview_markdown: sections.append(overview_markdown) + retained_urls.append(page_url) + else: + overview_reason = ( + "overview_omitted_by_source_policy" if _ref_prefix(ref.ref) in {"ES", "MIB"} else "empty_overview" + ) + omitted_sections.append(OmittedSection(url=page_url, reason=overview_reason)) - for url in chapter_urls: + for url in chapter_links.accepted: if _is_skipped_chapter(url): + omitted_sections.append(OmittedSection(url=url, reason="non_content_chapter")) continue chapter = client.get(url) chapter.raise_for_status() markdown = _chapter_markdown(chapter.text, link_mode=link_mode) if markdown: sections.append(markdown) + retained_urls.append(url) + else: + omitted_sections.append(OmittedSection(url=url, reason="empty_chapter")) content = "\n\n".join(sections).strip() if not content: raise NiceFetchError(f"No readable content for guidance '{ref.ref}'") - return content, len(sections), title + transformations = [ + "canonicalize_chapter_urls", + "convert_html_to_markdown", + "drop_numeric_citation_markers", + "filter_overview_boilerplate", + "normalize_numbered_headings", + "normalize_whitespace", + ] + if link_mode is LinkMode.STRIP: + transformations.append("strip_links") + receipt = GuidelineExtractionReceipt( + content=content, + section_count=len(sections), + title=title, + discovered_count=1 + len(chapter_links.accepted) + len(chapter_links.rejected), + retained_urls=tuple(retained_urls), + omitted_sections=tuple(omitted_sections), + transformations=tuple(transformations), + ) + if not receipt.is_accounted(): + raise AssertionError(f"Incomplete extraction receipt for guidance '{ref.ref}'") + return receipt def scrape_guideline( @@ -332,19 +430,25 @@ def scrape_guideline( link_mode: Whether links are kept as markdown links or stripped to their visible text (default: LinkMode.KEEP). """ - content, section_count, title = build_guideline_text(client, ref, link_mode=link_mode) + receipt = _build_guideline_receipt(client, ref, link_mode=link_mode) return ScrapedDocument( source="nice", external_id=f"nice-{ref.slug}", - title=title, - url=ref.page_url, - content=content, - section_count=section_count, + title=receipt.title, + url=_validated_page_url(ref), + content=receipt.content, + section_count=receipt.section_count, metadata={ "ref": ref.ref, "slug": ref.slug, "prefix": _ref_prefix(ref.ref), "scrape_strategy": _scrape_strategy(ref), + "retained_urls": list(receipt.retained_urls), + "omitted_sections": [ + {"url": omitted.url, "reason": omitted.reason} for omitted in receipt.omitted_sections + ], + "transformations": list(receipt.transformations), + "discovered_section_count": receipt.discovered_count, }, ) @@ -362,6 +466,13 @@ def _page_url(*, ref: str, slug: str) -> str: return f"{BASE_URL}{_page_path(ref=ref, slug=slug)}" +def _validated_page_url(ref: GuidanceRef) -> str: + validated = guidance_ref_from_url(ref.page_url) + if validated.ref != ref.ref.upper() or validated.slug != ref.slug.lower(): + raise NiceFetchError(f"Guidance reference {ref.ref!r} does not match its NICE page URL {ref.page_url!r}") + return validated.page_url + + def _scrape_strategy(ref: GuidanceRef) -> str: prefix = _ref_prefix(ref.ref) if prefix in _ADVICE_PREFIXES: @@ -371,6 +482,7 @@ def _scrape_strategy(ref: GuidanceRef) -> str: return _NiceScrapeStrategy.CHAPTER.value +# lean-spec: AMFV.Scraping.ListingAccounting.source_total_is_not_exact_after_filtering def scrape_nice( *, documents: int | None, @@ -386,6 +498,9 @@ def scrape_nice( link_mode: Whether links are kept as markdown links or stripped to their visible text (default: LinkMode.KEEP). url: NICE source URL to scrape as a single document (default: None). + + Listing runs report an indeterminate total because NICE's source count + includes guidance types filtered out by AMFV. Single-URL runs report one. """ if url is not None: @@ -397,9 +512,8 @@ def scrape_url() -> Iterable[ScrapedDocument]: with default_client() as client: first_page = list_published_guidance(client, page=1) - total = first_page.total if documents is None or first_page.total is None else min(documents, first_page.total) return ScrapeRun( - total=total, + total=None, documents=scrape_listing_documents( documents=documents, client_factory=default_client, @@ -414,11 +528,13 @@ def scrape_url() -> Iterable[ScrapedDocument]: __all__ = [ "BASE_URL", "DOCUMENT_DELAY_SECONDS", + "GuidelineExtractionReceipt", "GuidanceListingPage", "NICE_DATASET_DISPLAY_NAME", "NICE_DATASET_NAME", "GuidanceRef", "NiceFetchError", + "OmittedSection", "build_guideline_text", "guidance_ref_from_url", "list_published_guidance", diff --git a/datasets/test/test_scraping_html.py b/datasets/test/test_scraping_html.py index d34a8fa3..3a7f3428 100644 --- a/datasets/test/test_scraping_html.py +++ b/datasets/test/test_scraping_html.py @@ -23,6 +23,32 @@ def test_absolute_unique_urls_normalizes_relative_urls() -> None: ) == ["https://example.org/guidance/ng1", "https://example.org/guidance/ng2"] +# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority +def test_absolute_unique_urls_enforces_authority_policy() -> None: + """Host policies reject lookalike paths, credentials, and unusual ports.""" + assert absolute_unique_urls( + [ + "/guidance/ng1/chapter/recommendations?tab=contents", + "https://evil.example/guidance/ng1/chapter/recommendations", + "https://user@www.nice.org.uk/guidance/ng1/chapter/credentials", + "https://www.nice.org.uk:444/guidance/ng1/chapter/port", + "javascript:/guidance/ng1/chapter/script", + "https://www.nice.org.uk/guidance/ng1/chapter/recommendations#duplicate", + ], + base_url="https://www.nice.org.uk", + allowed_hosts=("nice.org.uk", "www.nice.org.uk"), + ) == ["https://www.nice.org.uk/guidance/ng1/chapter/recommendations"] + + +def test_absolute_unique_urls_canonicalization_is_idempotent() -> None: + """Canonical URLs remain unchanged when normalized again.""" + first_pass = absolute_unique_urls( + ["/guidance/ng1?tab=contents#heading"], + base_url="https://example.org", + ) + assert absolute_unique_urls(first_pass, base_url="https://example.org") == first_pass + + def test_first_matching_urls_uses_first_xpath_with_matches() -> None: """URL extraction falls back across XPath selectors.""" html_text = """ @@ -39,6 +65,23 @@ def test_first_matching_urls_uses_first_xpath_with_matches() -> None: ) == ["https://example.org/first"] +def test_first_matching_urls_falls_back_when_policy_rejects_first_xpath() -> None: + """Rejected candidates do not prevent an accepted fallback selector.""" + html_text = """ + + +
Good
+ + """ + + assert first_matching_urls( + html_text, + xpaths=("//nav/a/@href", "//main/a/@href"), + base_url="https://www.nice.org.uk", + allowed_hosts=("nice.org.uk", "www.nice.org.uk"), + ) == ["https://www.nice.org.uk/guidance/ng1/chapter/good"] + + def test_document_title_uses_heading_and_strips_suffix() -> None: """Document titles are read from common title locations.""" html_text = "

Guideline | Guidance | NICE

Fallback" diff --git a/datasets/test/test_scraping_nice.py b/datasets/test/test_scraping_nice.py index e6b9f464..a0b146b1 100644 --- a/datasets/test/test_scraping_nice.py +++ b/datasets/test/test_scraping_nice.py @@ -1,17 +1,23 @@ """Tests for NICE scraping helpers.""" import json +from contextlib import nullcontext import httpx +import pytest +from amfv_datasets.scraping import nice as nice_module from amfv_datasets.scraping.html import LinkMode from amfv_datasets.scraping.nice import ( BASE_URL, GuidanceListingPage, GuidanceRef, + NiceFetchError, build_guideline_text, guidance_ref_from_url, list_published_guidance, + scrape_guideline, + scrape_nice, ) @@ -31,7 +37,7 @@ def test_list_published_guidance_parses_next_data_listing() -> None: { "guidanceRef": "TA999", "title": "Technology appraisal", - "pathAndQuery": "/guidance/ta999", + "pathAndQuery": "https://evil.example/guidance/ta999", }, { "guidanceRef": "QS1", @@ -305,3 +311,142 @@ def handler(request: httpx.Request) -> httpx.Response: "## Quality statements\n\n" "Statement text." ) + + +# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_respects_source_boundary +def test_chapter_discovery_rejects_cross_guidance_normalization() -> None: + """Canonicalization cannot move a chapter link into another guidance scope.""" + overview = """ + + """ + discovery = nice_module._chapter_links(overview, "ng1") + + assert discovery.accepted == ("https://www.nice.org.uk/guidance/ng1/chapter/recommendations",) + assert discovery.rejected == ( + nice_module.OmittedSection( + url="https://www.nice.org.uk/guidance/ng2/chapter/recommendations", + reason="out_of_scope_url", + ), + ) + + +# lean-spec-test: AMFV.Scraping.ExtractionReceipt.accounted_receipt_matches_disposition_count +def test_scrape_guideline_rejects_off_domain_chapter_and_records_omissions() -> None: + """Only allowed NICE chapters are fetched and every discovered omission is recorded.""" + pages = { + "https://www.nice.org.uk/guidance/ng1": """ + +

Guideline

+

Overview

+

Useful overview.

+ + + """, + "https://www.nice.org.uk/guidance/ng1/chapter/recommendations": """ +

1 Recommendation

Do the safe thing [1].

+ """, + } + fetched: list[str] = [] + + def handler(request: httpx.Request) -> httpx.Response: + url = str(request.url) + fetched.append(url) + return httpx.Response(200, text=pages[url]) + + client = httpx.Client(transport=httpx.MockTransport(handler)) + document = scrape_guideline( + client, + GuidanceRef( + ref="NG1", + slug="ng1", + title="NG1", + page_url="https://www.nice.org.uk/guidance/ng1", + ), + ) + + assert all("evil.example" not in url for url in fetched) + assert document.metadata["retained_urls"] == [ + "https://www.nice.org.uk/guidance/ng1", + "https://www.nice.org.uk/guidance/ng1/chapter/recommendations", + ] + assert document.metadata["omitted_sections"] == [ + { + "url": "https://evil.example/guidance/ng1/chapter/lookalike", + "reason": "unsafe_url", + }, + { + "url": "https://www.nice.org.uk/guidance/ng2/chapter/recommendations", + "reason": "out_of_scope_url", + }, + { + "url": "https://www.nice.org.uk/guidance/ng1/chapter/finding-more-information-and-committee-details", + "reason": "non_content_chapter", + }, + ] + assert document.metadata["transformations"] == [ + "canonicalize_chapter_urls", + "convert_html_to_markdown", + "drop_numeric_citation_markers", + "filter_overview_boilerplate", + "normalize_numbered_headings", + "normalize_whitespace", + ] + assert document.metadata["discovered_section_count"] == 5 + + +def test_scrape_guideline_rejects_off_domain_overview_before_fetch() -> None: + """Manually constructed references cannot redirect the overview fetch.""" + fetched: list[str] = [] + + def handler(request: httpx.Request) -> httpx.Response: + fetched.append(str(request.url)) + return httpx.Response(200, text="") + + client = httpx.Client(transport=httpx.MockTransport(handler)) + + with pytest.raises(NiceFetchError, match="NICE guidance URL"): + scrape_guideline( + client, + GuidanceRef( + ref="NG1", + slug="ng1", + title="Guideline", + page_url="https://evil.example/guidance/ng1", + ), + ) + + assert fetched == [] + + +# lean-spec-test: AMFV.Scraping.ListingAccounting.source_total_is_not_exact_after_filtering +def test_scrape_nice_does_not_claim_filtered_source_total(monkeypatch) -> None: + """A source count that includes filtered guidance is not an exact run total.""" + listing = GuidanceListingPage( + refs=[ + GuidanceRef( + ref="NG1", + slug="ng1", + title="Guideline", + page_url="https://www.nice.org.uk/guidance/ng1", + ) + ], + total=6, + ) + monkeypatch.setattr( + "amfv_datasets.scraping.nice.default_client", + lambda: nullcontext(object()), + ) + monkeypatch.setattr( + "amfv_datasets.scraping.nice.list_published_guidance", + lambda _client, page=1: listing, + ) + + assert scrape_nice(documents=5).total is None diff --git a/formal/AMFV.lean b/formal/AMFV.lean new file mode 100644 index 00000000..a123324c --- /dev/null +++ b/formal/AMFV.lean @@ -0,0 +1,9 @@ +import AMFV.Logic.Adversarial +import AMFV.Scraping.ExtractionReceipt +import AMFV.Scraping.ListingAccounting +import AMFV.Scraping.UrlPolicy +import AMFV.Verification.CacheAdmission +import AMFV.Verification.Evaluation +import AMFV.Verification.Receipt +import AMFV.Verification.Verdict +import AMFV.ProofBoundary diff --git a/formal/AMFV/Logic/Adversarial.lean b/formal/AMFV/Logic/Adversarial.lean new file mode 100644 index 00000000..d39e14a9 --- /dev/null +++ b/formal/AMFV/Logic/Adversarial.lean @@ -0,0 +1,29 @@ +set_option autoImplicit false + +namespace AMFV.Logic.Adversarial + +abbrev Gate (α : Type) := α → Bool + +def Blindspot {α : Type} (gate unsafePred : Gate α) : Prop := + ∃ candidate, unsafePred candidate = true ∧ gate candidate = true + +def Sound {α : Type} (gate unsafePred : Gate α) : Prop := + ∀ candidate, gate candidate = true → unsafePred candidate = false + +theorem witnessed_blindspot_refutes_sound {α : Type} {gate unsafePred : Gate α} + (witness : Blindspot gate unsafePred) : ¬Sound gate unsafePred := by + intro sound + obtain ⟨candidate, unsafeTrue, admitted⟩ := witness + have unsafeFalse := sound candidate admitted + simp_all + +def hardened {α : Type} (gate unsafePred : Gate α) : Gate α := + fun candidate => gate candidate && !unsafePred candidate + +theorem hardened_gate_rejects_unsafe {α : Type} (gate unsafePred : Gate α) : + Sound (hardened gate unsafePred) unsafePred := by + intro candidate admitted + simp [hardened] at admitted + exact admitted.2 + +end AMFV.Logic.Adversarial diff --git a/formal/AMFV/LogicalEval.lean b/formal/AMFV/LogicalEval.lean new file mode 100644 index 00000000..97c9243f --- /dev/null +++ b/formal/AMFV/LogicalEval.lean @@ -0,0 +1,158 @@ +import AMFV +import Lean + +set_option autoImplicit false + +namespace AMFV.LogicalEval + +open AMFV.Verification +open Lean + +def schemaVersion := "amfv.logic.v1" +def maxLogicalTime : Nat := 253402300799 + +def getField (json : Json) (name : String) : Except String Json := + json.getObjVal? name + +def getString (json : Json) (name : String) : Except String String := do + (← getField json name).getStr? + +def getNat (json : Json) (name : String) : Except String Nat := do + (← getField json name).getNat? + +def getLogicalTime (json : Json) (name : String) : Except String Nat := do + let value ← getNat json name + if value ≤ maxLogicalTime then + pure value + else + throw s!"logical timestamp {name} exceeds the supported UTC range" + +def getBool (json : Json) (name : String) : Except String Bool := do + (← getField json name).getBool? + +def getNatList (json : Json) (name : String) : Except String (List Nat) := do + let values ← (← getField json name).getArr? + values.toList.mapM Json.getNat? + +def parseVerdict (value : String) : Except String Verdict.Verdict := + match value with + | "strongly_supported" => .ok .stronglySupported + | "weakly_supported" => .ok .weaklySupported + | "unclear" => .ok .unclear + | "weakly_unsubstantiated" => .ok .weaklyUnsubstantiated + | "strongly_unsubstantiated" => .ok .stronglyUnsubstantiated + | _ => .error s!"unknown verdict {value}" + +def receiptViolations (receipt : Receipt.Receipt) : List String := + let unknown := + if Receipt.referencesKnownEvidence receipt then [] else ["unknown_evidence_id"] + let overlap := + if Receipt.evidenceDisjoint receipt then [] else ["overlapping_evidence_id"] + let duplicate := + if Receipt.evidenceUnique receipt then [] else ["duplicate_evidence_id"] + let extreme := + if Receipt.extremeVerdictHasWitness receipt then [] else ["extreme_verdict_without_witness"] + let directional := + if Receipt.directionalVerdictHasWitness receipt then [] else ["directional_verdict_without_witness"] + unknown ++ overlap ++ duplicate ++ extreme ++ directional + +def evaluateReceipt (json : Json) : Except String (List String) := do + let receipt : Receipt.Receipt := { + knownEvidence := ← getNatList json "known_evidence" + supporting := ← getNatList json "supporting" + contradicting := ← getNatList json "contradicting" + missingContext := ← getBool json "missing_context" + verdict := ← parseVerdict (← getString json "verdict") + } + pure (receiptViolations receipt) + +def cacheViolations (entry : CacheAdmission.Entry) (query : CacheAdmission.Query) : List String := + let claim := + if entry.claimKey == query.claimKey then [] else ["claim_mismatch"] + let scope := + if entry.scopeKey == query.scopeKey then [] else ["scope_mismatch"] + let evidence := + if entry.evidenceCount > 0 then [] else ["empty_evidence"] + let trace := + if entry.traceCount > 0 then [] else ["empty_trace"] + let future := + if entry.verifiedAt ≤ query.asOf then [] else ["verified_in_future"] + let stale := + if query.asOf ≤ entry.validUntil then [] else ["stale_entry"] + let interval := + if entry.verifiedAt ≤ entry.validUntil then [] else ["invalid_validity_interval"] + claim ++ scope ++ evidence ++ trace ++ interval ++ future ++ stale + +def evaluateCache (json : Json) : Except String (List String) := do + let entry : CacheAdmission.Entry := { + claimKey := ← getNat json "entry_claim_key" + scopeKey := ← getNat json "entry_scope_key" + verifiedAt := ← getLogicalTime json "verified_at" + validUntil := ← getLogicalTime json "valid_until" + evidenceCount := ← getNat json "evidence_count" + traceCount := ← getNat json "trace_count" + } + let query : CacheAdmission.Query := { + claimKey := ← getNat json "query_claim_key" + scopeKey := ← getNat json "query_scope_key" + asOf := ← getLogicalTime json "as_of" + } + pure (cacheViolations entry query) + +def evaluationViolations (result : Evaluation.CaseResult) : List String := + let retrieval := + if result.retrievalHit then [] else ["retrieval_miss"] + let verdict := + if result.verdictMatch then [] else ["verdict_mismatch"] + let score := + if result.scorePass then [] else ["score_failure"] + retrieval ++ verdict ++ score + +def evaluateCase (json : Json) : Except String (List String) := do + let result : Evaluation.CaseResult := { + retrievalHit := ← getBool json "retrieval_hit" + verdictMatch := ← getBool json "verdict_match" + scorePass := ← getBool json "score_pass" + } + pure (evaluationViolations result) + +def evaluate (json : Json) : Except String (List String) := do + let schema ← getString json "schema" + if schema != schemaVersion then + throw s!"unsupported schema {schema}" + match ← getString json "kind" with + | "verifier_receipt" => evaluateReceipt json + | "cache_admission" => evaluateCache json + | "evaluation_case" => evaluateCase json + | kind => throw s!"unknown logical record kind {kind}" + +def response (violations : List String) : Json := + Json.mkObj [ + ("valid", Json.bool violations.isEmpty), + ("violations", Json.arr (violations.toArray.map Json.str)) + ] + +def errorResponse (message : String) : Json := + Json.mkObj [ + ("valid", Json.bool false), + ("violations", Json.arr #[Json.str "invalid_input"]), + ("error", Json.str message) + ] + +def evaluateLine (line : String) : Json := + match Json.parse line >>= evaluate with + | .ok violations => response violations + | .error message => errorResponse message + +partial def processLines (input : IO.FS.Stream) : IO Unit := do + let line ← input.getLine + if line.isEmpty then + pure () + else + IO.println (Json.compress (evaluateLine line.trimAscii.toString)) + processLines input + +end AMFV.LogicalEval + +def main : IO Unit := do + AMFV.LogicalEval.processLines (← IO.getStdin) diff --git a/formal/AMFV/ProofBoundary.lean b/formal/AMFV/ProofBoundary.lean new file mode 100644 index 00000000..d848ebe9 --- /dev/null +++ b/formal/AMFV/ProofBoundary.lean @@ -0,0 +1,22 @@ +set_option autoImplicit false + +namespace AMFV.ProofBoundary + +structure StructuralReceipt where + safeAuthority : Bool + accounted : Bool + +def structurallyValid (receipt : StructuralReceipt) : Bool := + receipt.safeAuthority && receipt.accounted + +def validReceipt : StructuralReceipt where + safeAuthority := true + accounted := true + +theorem structural_validity_does_not_force_medical_truth : + ¬(∀ medicalTruth : Bool, structurallyValid validReceipt = true → medicalTruth = true) := by + intro forcesTruth + have falseIsTrue := forcesTruth false rfl + contradiction + +end AMFV.ProofBoundary diff --git a/formal/AMFV/Scraping/ExtractionReceipt.lean b/formal/AMFV/Scraping/ExtractionReceipt.lean new file mode 100644 index 00000000..5d7cd825 --- /dev/null +++ b/formal/AMFV/Scraping/ExtractionReceipt.lean @@ -0,0 +1,28 @@ +set_option autoImplicit false + +namespace AMFV.Scraping.ExtractionReceipt + +structure Receipt where + discovered : Nat + retained : Nat + omitted : Nat + +def Accounted (receipt : Receipt) : Prop := + receipt.discovered = receipt.retained + receipt.omitted + +def silentOmission : Receipt where + discovered := 3 + retained := 1 + omitted := 1 + +theorem silent_omission_is_not_accounted : + ¬Accounted silentOmission := by + change ¬(3 = 2) + decide + +theorem accounted_receipt_matches_disposition_count (receipt : Receipt) + (isAccounted : Accounted receipt) : + receipt.discovered = receipt.retained + receipt.omitted := + isAccounted + +end AMFV.Scraping.ExtractionReceipt diff --git a/formal/AMFV/Scraping/ListingAccounting.lean b/formal/AMFV/Scraping/ListingAccounting.lean new file mode 100644 index 00000000..3e643b92 --- /dev/null +++ b/formal/AMFV/Scraping/ListingAccounting.lean @@ -0,0 +1,31 @@ +set_option autoImplicit false + +namespace AMFV.Scraping.ListingAccounting + +structure Inventory where + sourceTotal : Nat + eligibleTotal : Nat + emittedTotal : Nat + +def HonestExactTotal (inventory : Inventory) : Prop := + inventory.sourceTotal = inventory.eligibleTotal + +def filteredExample : Inventory where + sourceTotal := 6 + eligibleTotal := 5 + emittedTotal := 5 + +theorem source_total_is_not_exact_after_filtering : + ¬HonestExactTotal filteredExample := by + change ¬(6 = 5) + decide + +theorem emitted_under_cap (eligible cap : Nat) : + Nat.min eligible cap ≤ cap := + Nat.min_le_right eligible cap + +theorem emitted_not_above_eligible (eligible cap : Nat) : + Nat.min eligible cap ≤ eligible := + Nat.min_le_left eligible cap + +end AMFV.Scraping.ListingAccounting diff --git a/formal/AMFV/Scraping/UrlPolicy.lean b/formal/AMFV/Scraping/UrlPolicy.lean new file mode 100644 index 00000000..e79a08f0 --- /dev/null +++ b/formal/AMFV/Scraping/UrlPolicy.lean @@ -0,0 +1,104 @@ +set_option autoImplicit false + +namespace AMFV.Scraping.UrlPolicy + +inductive Scheme where + | http + | https + | other + deriving DecidableEq + +inductive Authority where + | nice + | other + deriving DecidableEq + +structure Candidate where + scheme : Scheme + authority : Authority + chapterPath : Bool + sameGuidance : Bool + hasCredentials : Bool + hasNondefaultPort : Bool + hasQuery : Bool + hasFragment : Bool + deriving DecidableEq + +def canonicalize (candidate : Candidate) : Candidate := + { candidate with hasQuery := false, hasFragment := false } + +def pathOnlyGate (candidate : Candidate) : Bool := + candidate.chapterPath + +def acceptedChapter (candidate : Candidate) : Bool := + candidate.chapterPath && + candidate.sameGuidance && + (candidate.scheme == .http || candidate.scheme == .https) && + candidate.authority == .nice && + !candidate.hasCredentials && + !candidate.hasNondefaultPort + +theorem canonicalize_idempotent (candidate : Candidate) : + canonicalize (canonicalize candidate) = canonicalize candidate := by + cases candidate + rfl + +theorem canonicalize_preserves_authority (candidate : Candidate) : + (canonicalize candidate).authority = candidate.authority := by + rfl + +theorem accepted_chapter_has_allowed_authority (candidate : Candidate) + (accepted : acceptedChapter candidate = true) : + candidate.authority = .nice := by + cases candidate with + | mk scheme authority chapterPath sameGuidance hasCredentials hasNondefaultPort hasQuery hasFragment => + cases authority with + | nice => rfl + | other => + cases scheme <;> + cases chapterPath <;> + cases sameGuidance <;> + cases hasCredentials <;> + cases hasNondefaultPort <;> + cases accepted + +theorem accepted_chapter_matches_guidance (candidate : Candidate) + (accepted : acceptedChapter candidate = true) : + candidate.sameGuidance = true := by + cases candidate with + | mk scheme authority chapterPath sameGuidance hasCredentials hasNondefaultPort hasQuery hasFragment => + cases sameGuidance with + | false => + cases scheme <;> + cases authority <;> + cases chapterPath <;> + cases hasCredentials <;> + cases hasNondefaultPort <;> + cases accepted + | true => rfl + +theorem accepted_chapter_respects_source_boundary (candidate : Candidate) + (accepted : acceptedChapter candidate = true) : + candidate.authority = .nice ∧ candidate.sameGuidance = true := + ⟨accepted_chapter_has_allowed_authority candidate accepted, + accepted_chapter_matches_guidance candidate accepted⟩ + +def offAuthorityChapter : Candidate where + scheme := .https + authority := .other + chapterPath := true + sameGuidance := true + hasCredentials := false + hasNondefaultPort := false + hasQuery := false + hasFragment := false + +theorem path_only_gate_has_off_authority_blindspot : + pathOnlyGate offAuthorityChapter = true ∧ offAuthorityChapter.authority = .other := by + decide + +theorem hardened_gate_closes_off_authority_blindspot : + acceptedChapter offAuthorityChapter = false := by + decide + +end AMFV.Scraping.UrlPolicy diff --git a/formal/AMFV/Verification/CacheAdmission.lean b/formal/AMFV/Verification/CacheAdmission.lean new file mode 100644 index 00000000..a3b7930c --- /dev/null +++ b/formal/AMFV/Verification/CacheAdmission.lean @@ -0,0 +1,50 @@ +set_option autoImplicit false + +namespace AMFV.Verification.CacheAdmission + +structure Entry where + claimKey : Nat + scopeKey : Nat + verifiedAt : Nat + validUntil : Nat + evidenceCount : Nat + traceCount : Nat + +structure Query where + claimKey : Nat + scopeKey : Nat + asOf : Nat + +def admissible (entry : Entry) (query : Query) : Bool := + entry.claimKey == query.claimKey && + entry.scopeKey == query.scopeKey && + entry.evidenceCount > 0 && + entry.traceCount > 0 && + entry.verifiedAt ≤ query.asOf && + query.asOf ≤ entry.validUntil + +def staleEntry : Entry where + claimKey := 7 + scopeKey := 3 + verifiedAt := 10 + validUntil := 20 + evidenceCount := 2 + traceCount := 1 + +def lateQuery : Query where + claimKey := 7 + scopeKey := 3 + asOf := 21 + +def hashAndScopeOnly (entry : Entry) (query : Query) : Bool := + entry.claimKey == query.claimKey && entry.scopeKey == query.scopeKey + +theorem hash_scope_only_accepts_stale_entry : + hashAndScopeOnly staleEntry lateQuery = true := by + decide + +theorem admissible_rejects_stale_entry : + admissible staleEntry lateQuery = false := by + decide + +end AMFV.Verification.CacheAdmission diff --git a/formal/AMFV/Verification/Evaluation.lean b/formal/AMFV/Verification/Evaluation.lean new file mode 100644 index 00000000..c9729167 --- /dev/null +++ b/formal/AMFV/Verification/Evaluation.lean @@ -0,0 +1,35 @@ +set_option autoImplicit false + +namespace AMFV.Verification.Evaluation + +structure CaseResult where + retrievalHit : Bool + verdictMatch : Bool + scorePass : Bool + +def casePass (result : CaseResult) : Bool := + result.retrievalHit && result.verdictMatch && result.scorePass + +def twoFactorPass (result : CaseResult) : Bool := + result.retrievalHit && result.scorePass + +def wrongVerdict : CaseResult where + retrievalHit := true + verdictMatch := false + scorePass := true + +theorem case_pass_implies_all_checks (result : CaseResult) + (passed : casePass result = true) : + result.retrievalHit = true ∧ result.verdictMatch = true ∧ result.scorePass = true := by + simp [casePass] at passed + exact ⟨passed.1.1, passed.1.2, passed.2⟩ + +theorem two_factor_gate_accepts_wrong_verdict : + twoFactorPass wrongVerdict = true := by + decide + +theorem three_factor_gate_rejects_wrong_verdict : + casePass wrongVerdict = false := by + decide + +end AMFV.Verification.Evaluation diff --git a/formal/AMFV/Verification/Receipt.lean b/formal/AMFV/Verification/Receipt.lean new file mode 100644 index 00000000..f51ef6fa --- /dev/null +++ b/formal/AMFV/Verification/Receipt.lean @@ -0,0 +1,107 @@ +import AMFV.Verification.Verdict + +set_option autoImplicit false + +namespace AMFV.Verification.Receipt + +open AMFV.Verification.Verdict + +structure Receipt where + knownEvidence : List Nat + supporting : List Nat + contradicting : List Nat + missingContext : Bool + verdict : Verdict + +def containsNat (identifier : Nat) : List Nat → Bool + | [] => false + | candidate :: rest => Nat.beq identifier candidate || containsNat identifier rest + +def referencesKnownEvidence (receipt : Receipt) : Bool := + receipt.supporting.all (fun identifier => containsNat identifier receipt.knownEvidence) && + receipt.contradicting.all (fun identifier => containsNat identifier receipt.knownEvidence) + +def evidenceDisjoint (receipt : Receipt) : Bool := + receipt.supporting.all (fun identifier => !containsNat identifier receipt.contradicting) + +def noDuplicates : List Nat → Bool + | [] => true + | identifier :: rest => !containsNat identifier rest && noDuplicates rest + +def evidenceUnique (receipt : Receipt) : Bool := + noDuplicates receipt.supporting && noDuplicates receipt.contradicting + +def extremeVerdictHasWitness (receipt : Receipt) : Bool := + match receipt.verdict with + | .stronglySupported => + !receipt.supporting.isEmpty && receipt.contradicting.isEmpty && !receipt.missingContext + | .stronglyUnsubstantiated => + !receipt.contradicting.isEmpty && receipt.supporting.isEmpty && !receipt.missingContext + | .weaklySupported => true + | .unclear => true + | .weaklyUnsubstantiated => true + +def directionalVerdictHasWitness (receipt : Receipt) : Bool := + match receipt.verdict with + | .weaklySupported => !receipt.supporting.isEmpty + | .weaklyUnsubstantiated => !receipt.contradicting.isEmpty + | .stronglySupported => true + | .unclear => true + | .stronglyUnsubstantiated => true + +def valid (receipt : Receipt) : Bool := + referencesKnownEvidence receipt && + evidenceDisjoint receipt && + evidenceUnique receipt && + extremeVerdictHasWitness receipt && + directionalVerdictHasWitness receipt + +def unknownEvidenceReceipt : Receipt where + knownEvidence := [1] + supporting := [2] + contradicting := [] + missingContext := false + verdict := .stronglySupported + +def overlappingEvidenceReceipt : Receipt where + knownEvidence := [1] + supporting := [1] + contradicting := [1] + missingContext := false + verdict := .unclear + +def unwitnessedStrongReceipt : Receipt where + knownEvidence := [] + supporting := [] + contradicting := [] + missingContext := true + verdict := .stronglySupported + +def duplicateEvidenceReceipt : Receipt where + knownEvidence := [1] + supporting := [1, 1] + contradicting := [] + missingContext := false + verdict := .weaklySupported + +theorem unknown_evidence_invalid : valid unknownEvidenceReceipt = false := by + rfl + +theorem overlapping_evidence_invalid : valid overlappingEvidenceReceipt = false := by + rfl + +theorem strong_verdict_requires_witness : valid unwitnessedStrongReceipt = false := by + rfl + +theorem duplicate_evidence_invalid : valid duplicateEvidenceReceipt = false := by + rfl + +theorem known_counterexamples_invalid : + valid unknownEvidenceReceipt = false ∧ + valid overlappingEvidenceReceipt = false ∧ + valid duplicateEvidenceReceipt = false ∧ + valid unwitnessedStrongReceipt = false := by + exact ⟨unknown_evidence_invalid, overlapping_evidence_invalid, duplicate_evidence_invalid, + strong_verdict_requires_witness⟩ + +end AMFV.Verification.Receipt diff --git a/formal/AMFV/Verification/Verdict.lean b/formal/AMFV/Verification/Verdict.lean new file mode 100644 index 00000000..7044de7f --- /dev/null +++ b/formal/AMFV/Verification/Verdict.lean @@ -0,0 +1,35 @@ +set_option autoImplicit false + +namespace AMFV.Verification.Verdict + +inductive Verdict where + | stronglySupported + | weaklySupported + | unclear + | weaklyUnsubstantiated + | stronglyUnsubstantiated + deriving DecidableEq + +def score : Verdict → Int + | .stronglySupported => 2 + | .weaklySupported => 1 + | .unclear => 0 + | .weaklyUnsubstantiated => -1 + | .stronglyUnsubstantiated => -2 + +def reverse : Verdict → Verdict + | .stronglySupported => .stronglyUnsubstantiated + | .weaklySupported => .weaklyUnsubstantiated + | .unclear => .unclear + | .weaklyUnsubstantiated => .weaklySupported + | .stronglyUnsubstantiated => .stronglySupported + +theorem reverse_score (verdict : Verdict) : + score (reverse verdict) = -score verdict := by + cases verdict <;> decide + +theorem unclear_is_not_strongly_unsubstantiated : + Verdict.unclear ≠ Verdict.stronglyUnsubstantiated := by + decide + +end AMFV.Verification.Verdict diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 00000000..f3ad9c4d --- /dev/null +++ b/formal/README.md @@ -0,0 +1,39 @@ +# AMFV logical evaluation + +This directory contains small, executable models of AMFV's structural +invariants. The models use Lean's standard library only and are pinned to Lean +4.32.0. + +The canonical developer guide is [`../FORMAL_LOGIC.md`](../FORMAL_LOGIC.md). +Read it before adding a model, changing the JSONL protocol, linking a Python +boundary, or updating the Lean toolchain. + +```sh +lake build --wfail +python3 tools/check_lean_specs.py +python3 tools/check_logic_fixtures.py +``` + +## Quick reference + +A Python annotation such as +`# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority` +links an implementation decision to a named theorem. Lean proves the theorem +about the model. Python regression tests exercise the corresponding production +behavior against the same counterexample and carry a matching +`# lean-spec-test:` annotation. CI requires each target to be a theorem with an +empty axiom footprint. The annotation does not claim that Lean verifies Python +bytecode, arbitrary web pages, clinical truth, or corpus completeness. + +Keep theorems narrow and operational. The repository checker rejects Lake +dependencies, proof placeholders, assumption declarations, tagged definitions, +tagged theorems with axiom dependencies, and proof links without paired runtime +tests. + +## Logical evaluator + +`lake exe amfv_logic` reads one `amfv.logic.v1` JSON object per line and emits +one structural result per line. Supported kinds are `verifier_receipt`, +`cache_admission`, and `evaluation_case`. The evaluator reports stable +violation codes for CI and development tooling. It does not judge medical +claims or evidence content. diff --git a/formal/fixtures/logical-eval.jsonl b/formal/fixtures/logical-eval.jsonl new file mode 100644 index 00000000..82b9f3f4 --- /dev/null +++ b/formal/fixtures/logical-eval.jsonl @@ -0,0 +1,16 @@ +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1,2],"supporting":[1],"contradicting":[],"missing_context":false,"verdict":"strongly_supported","expected_valid":true,"expected_violations":[]} +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[2],"contradicting":[],"missing_context":false,"verdict":"strongly_supported","expected_valid":false,"expected_violations":["unknown_evidence_id"]} +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[1],"contradicting":[1],"missing_context":false,"verdict":"unclear","expected_valid":false,"expected_violations":["overlapping_evidence_id"]} +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[1,1],"contradicting":[],"missing_context":false,"verdict":"weakly_supported","expected_valid":false,"expected_violations":["duplicate_evidence_id"]} +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[],"supporting":[],"contradicting":[],"missing_context":true,"verdict":"strongly_supported","expected_valid":false,"expected_violations":["extreme_verdict_without_witness"]} +{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[],"supporting":[],"contradicting":[],"missing_context":false,"verdict":"weakly_supported","expected_valid":false,"expected_violations":["directional_verdict_without_witness"]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":true,"expected_violations":[]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7e0,"entry_scope_key":3e0,"verified_at":1e1,"valid_until":2e1,"evidence_count":2e0,"trace_count":1e0,"query_claim_key":7e0,"query_scope_key":3e0,"as_of":1.5e1,"expected_valid":true,"expected_violations":[]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":21,"expected_valid":false,"expected_violations":["stale_entry"]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":0,"trace_count":0,"query_claim_key":7,"query_scope_key":4,"as_of":9,"expected_valid":false,"expected_violations":["scope_mismatch","empty_evidence","empty_trace","verified_in_future"]} +{"schema":"amfv.logic.v1","kind":"evaluation_case","retrieval_hit":true,"verdict_match":true,"score_pass":true,"expected_valid":true,"expected_violations":[]} +{"schema":"amfv.logic.v1","kind":"evaluation_case","retrieval_hit":true,"verdict_match":false,"score_pass":true,"expected_valid":false,"expected_violations":["verdict_mismatch"]} +{"schema":"amfv.logic.v2","kind":"evaluation_case","retrieval_hit":true,"verdict_match":true,"score_pass":true,"expected_valid":false,"expected_violations":["invalid_input"]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":null,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":false,"expected_violations":["invalid_input"]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":20,"valid_until":10,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":false,"expected_violations":["invalid_validity_interval","verified_in_future","stale_entry"]} +{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":1000000000000000000000000000000,"valid_until":1000000000000000000000000000001,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":1000000000000000000000000000000,"expected_valid":false,"expected_violations":["invalid_input"]} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 00000000..cef90821 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "amfv", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 00000000..ebdf9d0d --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,12 @@ +name = "amfv" +version = "0.1.0" +defaultTargets = ["AMFV", "amfv_logic"] + +[[lean_lib]] +name = "AMFV" +srcDir = "formal" + +[[lean_exe]] +name = "amfv_logic" +srcDir = "formal" +root = "AMFV.LogicalEval" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 00000000..94b9f495 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0 diff --git a/tools/check_lean_specs.py b/tools/check_lean_specs.py new file mode 100644 index 00000000..0649c8a1 --- /dev/null +++ b/tools/check_lean_specs.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Check Lean proof hygiene and resolve Python ``lean-spec`` annotations.""" + +from __future__ import annotations + +import json +import re +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +FORMAL_ROOT = ROOT / "formal" +PYTHON_ROOTS = ("baseline", "datasets", "decomposer", "search", "training", "utils", "verifier") +TAG_RE = re.compile(r"^\s*#\s*lean-spec:\s*([A-Za-z_][A-Za-z0-9_.]*)\s*$") +TEST_TAG_RE = re.compile(r"^\s*#\s*lean-spec-test:\s*([A-Za-z_][A-Za-z0-9_.]*)\s*$") +DECL_RE = re.compile(r"^\s*(?:async\s+)?(?:def|class)\s+[A-Za-z_][A-Za-z0-9_]*") +FORBIDDEN_RE = re.compile( + r"^\s*(?:(?:private|protected|noncomputable|unsafe)\s+)*(?:axiom|constant|opaque)\s+" + r"|\b(?:by\s+)?(?:sorry|admit)\b" +) + + +def fail(message: str) -> None: + """Print a checker failure and terminate.""" + raise SystemExit(message) + + +def check_formal_hygiene() -> None: + """Reject proof placeholders and assumption declarations.""" + failures: list[str] = [] + for path in sorted(FORMAL_ROOT.rglob("*.lean")): + for line_number, line in enumerate(path.read_text().splitlines(), start=1): + code = line.split("--", 1)[0] + if FORBIDDEN_RE.search(code): + failures.append(f"{path.relative_to(ROOT)}:{line_number}: forbidden proof escape") + if failures: + fail("\n".join(failures)) + manifest = json.loads((ROOT / "lake-manifest.json").read_text()) + if manifest.get("packages") != []: + fail("formal library must remain dependency-free") + + +def collect_tags() -> list[str]: + """Collect annotations and ensure they are attached to Python declarations.""" + tags: list[str] = [] + test_tags: set[str] = set() + failures: list[str] = [] + for source_root in PYTHON_ROOTS: + for path in sorted((ROOT / source_root).rglob("*.py")): + lines = path.read_text().splitlines() + for index, line in enumerate(lines): + match = TAG_RE.match(line) + test_match = TEST_TAG_RE.match(line) + if test_match: + if index + 1 >= len(lines) or not DECL_RE.match(lines[index + 1]): + failures.append( + f"{path.relative_to(ROOT)}:{index + 1}: " + "lean-spec-test must immediately precede a test function" + ) + test_tags.add(test_match.group(1)) + if not match: + continue + if index + 1 >= len(lines) or not DECL_RE.match(lines[index + 1]): + failures.append( + f"{path.relative_to(ROOT)}:{index + 1}: lean-spec must immediately precede a function or class" + ) + tags.append(match.group(1)) + if failures: + fail("\n".join(failures)) + if not tags: + fail("no lean-spec annotations found") + untested_tags = sorted(set(tags) - test_tags) + if untested_tags: + fail("lean-spec annotations without paired runtime tests:\n" + "\n".join(untested_tags)) + return tags + + +def resolve_tags(tags: list[str]) -> None: + """Ask Lean to resolve every referenced declaration.""" + source = "import AMFV\n\n" + "\n".join( + f"set_option pp.proofs false in\n#print {tag}\n#print axioms {tag}" for tag in sorted(set(tags)) + ) + source += "\n" + with tempfile.NamedTemporaryFile("w", suffix=".lean", dir=ROOT, delete=False) as handle: + handle.write(source) + check_path = Path(handle.name) + try: + result = subprocess.run( + ["lake", "env", "lean", str(check_path)], + cwd=ROOT, + text=True, + capture_output=True, + check=False, + ) + finally: + check_path.unlink(missing_ok=True) + if result.returncode: + sys.stderr.write(result.stdout) + sys.stderr.write(result.stderr) + fail("one or more lean-spec annotations do not resolve") + for tag in set(tags): + if f"theorem {tag} " not in result.stdout: + fail(f"lean-spec target is not a theorem: {tag}") + if f"'{tag}' depends on axioms:" in result.stdout: + fail(f"lean-spec theorem has an axiom dependency: {tag}") + + +def main() -> None: + """Run all formal-source checks.""" + check_formal_hygiene() + resolve_tags(collect_tags()) + + +if __name__ == "__main__": + main() diff --git a/tools/check_logic_fixtures.py b/tools/check_logic_fixtures.py new file mode 100644 index 00000000..fe7c4ef8 --- /dev/null +++ b/tools/check_logic_fixtures.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Run shared JSONL fixtures through the Lean logical evaluator.""" + +from __future__ import annotations + +import json +import subprocess +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +FIXTURES = ROOT / "formal" / "fixtures" / "logical-eval.jsonl" + + +def main() -> None: + """Evaluate every fixture and compare stable result fields.""" + lines = [line for line in FIXTURES.read_text().splitlines() if line.strip()] + records = [json.loads(line) for line in lines] + process = subprocess.run( + ["lake", "exe", "amfv_logic"], + cwd=ROOT, + input="\n".join(lines) + "\n", + text=True, + capture_output=True, + check=False, + ) + if process.returncode: + raise SystemExit(process.stderr or process.stdout) + outputs = [json.loads(line) for line in process.stdout.splitlines() if line.strip()] + if len(outputs) != len(records): + raise SystemExit(f"expected {len(records)} oracle responses; got {len(outputs)}") + failures: list[str] = [] + for index, (record, output) in enumerate(zip(records, outputs, strict=True), start=1): + expected = { + "valid": record["expected_valid"], + "violations": record["expected_violations"], + } + actual = { + "valid": output.get("valid"), + "violations": output.get("violations"), + } + if actual != expected: + failures.append(f"fixture {index}: expected {expected!r}; got {actual!r}") + if failures: + raise SystemExit("\n".join(failures)) + print(f"{len(records)} logical-evaluation fixtures passed") + + +if __name__ == "__main__": + main()