check_sequence_history.py

#!/usr/bin/env python3
"""Check the preserved sequence-contract chronology used by review Run 06."""

from html import unescape
from html.parser import HTMLParser
import json
from pathlib import Path


ROOT = Path(__file__).resolve().parent / "history" / "objects"

SNAPSHOTS = {
    "direct_early": "0e0780fa6108cdc19de4af0d9d9916431f9e5f85e88ffc7441a1670a4659c519",
    "direct_transitional": "8ed9827ff880190b3800056b2613bcb1fae8aad1d7389181db46a9ba1e917011",
    "direct_withdrawn": "066e3014a124688aa4a40e232f07bfabe81811d2fd901984e920e930a0d26399",
    "direct_fixed_layout": "276700ba2d6ffb6f3c3dfa459db312669cfd7b9ae4bd935615b5e4d38a1f974f",
    "direct_normalized": "67511aeec6a00f705b647ed90fdc71980128eb5b4eba149142e412527d70056a",
    "direct_restored": "d9c2d333c9e8cf300b16c1b480f3c1aadc0fb22fc2fd0029ed19cbd449e8a37b",
    "direct_radius_withdrawn": "1d05a3bbfd6edfc6e1a7393b95491b8f15b6c012fa34fda45612d5a6a73ae6df",
    "direct_draft_5": "d34d79ed8bffa82a7e9c2ce726bba32d131c4ffbe9a93b90fb0fd3cd929fd6c3",
    "causal_before_restoration": "d3859784f333803c4881cfbbf6a42d69e4485f940695da55cbad07bcfbc5e0ec",
    "causal_at_restoration": "2b0910f423c0a56136a7d1c293c57ff5f6361ee40bf5d777aa4d1da7aaaae716",
}


class TextExtractor(HTMLParser):
    def __init__(self):
        super().__init__()
        self.parts = []

    def handle_data(self, data):
        self.parts.append(data)


def text_for(name):
    raw = (ROOT / f"{SNAPSHOTS[name]}.txt").read_text(encoding="utf-8")
    parser = TextExtractor()
    parser.feed(raw)
    return " ".join(unescape(" ".join(parser.parts)).split())


def has(text, phrase):
    return phrase.casefold() in text.casefold()


texts = {name: text_for(name) for name in SNAPSHOTS}

checks = {
    "early_treated_modern_source_as_nonpremise": has(
        texts["direct_early"],
        "The published modern deque implementation is a comparison and source check, not the premise of the proof",
    ),
    "early_claimed_theorem_12_2": has(texts["direct_early"], "Theorem 12.2"),
    "transitional_opening_qualified_route": has(
        texts["direct_transitional"], "the complete route is therefore not presently claimed as a theorem"
    ),
    "transitional_body_still_retained_theorem_label": has(
        texts["direct_transitional"], "Theorem 12.2 (Direct palindrome scaffolding)"
    ),
    "withdrawal_explicit": has(texts["direct_withdrawn"], "Former Theorem 12.2 — withdrawn as a theorem"),
    "fixed_layout_still_awaited_end_to_end_audit": has(
        texts["direct_fixed_layout"], "has not received a fresh end-to-end audit"
    ),
    "normalization_gap_identified": has(
        texts["direct_normalized"], "whole-client source-to-plan normalization obligation open"
    ),
    "abstract_model_restored": has(
        texts["direct_restored"], "second proof in the stated abstract source-record model"
    ),
    "manual_address_premise_visible": has(
        texts["direct_restored"], "manual old-address bounds remain its weakest quantitative premise"
    ),
    "radius_certificate_withdrawn": has(
        texts["direct_radius_withdrawn"], "Later correction: numerical radius withdrawn"
    ),
    "radius_withdrawal_cites_old_fresh_gap": has(
        texts["direct_radius_withdrawn"], "old/fresh provenance"
    ),
    "draft_5_theorem_is_conditional": has(
        texts["direct_draft_5"], "For a persistent sequence implementation satisfying the contract of Section 11.1"
    ),
    "draft_5_calls_source_arguments_informal": has(
        texts["direct_draft_5"], "These are informal source-level arguments for the contract in Section 11.1"
    ),
    "causal_before_restoration_kept_obligations_open": has(
        texts["causal_before_restoration"], "Those obligations remain open"
    ),
    "causal_at_restoration_claimed_explicit_implementation": has(
        texts["causal_at_restoration"], "an explicit strict source-record implementation, its resource certificate"
    ),
}

assert all(checks.values()), [name for name, passed in checks.items() if not passed]

result = {
    "status": "pass",
    "snapshots_checked": len(SNAPSHOTS),
    "assertions_checked": len(checks),
    "checks": checks,
    "conclusion": {
        "direct_theorem_withdrawal_was_historical": True,
        "direct_current_theorem_is_conditional": True,
        "numerical_radius_remains_withdrawn": True,
        "causal_companion_wording_froze_at_restoration_stage": True,
        "paper_files_modified_by_this_check": False,
    },
}

print(json.dumps(result, indent=2, sort_keys=True))