#!/usr/bin/env python3
"""Find retracted claims that are still stated unqualified somewhere else.

This project's working rule is "record retractions in place and propagate them
to referencing documents". Three separate bugs in this tree turned out to be a
correction that existed but had not been propagated -- including a FIDELITY-NOTES
section that flatly contradicted a retraction later in the SAME file.

Mechanism (the signal that caught that one): a retraction usually *quotes* the
claim it is killing, e.g.

    state that "Unicorn has no ARM MMU, so everything stays flat/identity" ...
    **Both are wrong.**

So: collect quoted spans that appear near a retraction marker, then look for
those same spans elsewhere in the tree. Any occurrence that is NOT itself near a
retraction marker is a candidate un-propagated claim.

Heuristic and deliberately noisy in the safe direction -- it reports candidates
for a human to judge, it does not edit anything. Exit status is always 0; this
is a review aid, not a gate.

VALIDATED AGAINST A POSITIVE CONTROL, because an unvalidated detector reporting
"nothing found" is worthless. Run against a worktree at commit 4a04207 (before
the MMU retraction was propagated) it reports exactly one candidate -- the real
one, `FIDELITY-NOTES.md:228` -- with no false positives. Against the current
tree it reports nothing. If you change the heuristics, re-run that control:

    git worktree add /tmp/x 4a04207 && cp psp_out/check_retractions.py /tmp/x/psp_out/
    (cd /tmp/x && python3 psp_out/check_retractions.py)   # must find the MMU claim

KNOWN BLIND SPOTS -- do not read a clean run as "the docs are consistent":

  * **Paraphrases are missed.** It matches a quoted claim only where it is
    restated *verbatim*. The same MMU retraction was ALSO contradicted by
    "page tables programmed but not honoured (Unicorn has none)" in
    `FINDING-FULL-SOS-BOOT-IN-EMULATOR.md`, which this tool does not catch
    because the wording differs. That one was found by hand.
  * **Corrections never phrased as a retraction are invisible.** Two of the
    three real cases in this tree were of that kind: ASD recorded as "not
    loaded" long after the ring path could load it, and
    `fuzz_pss_differential.py` still using a calling convention that
    `verify_real_image.py` had already corrected. Neither quoted anything, so
    neither is detectable this way.

Usage:  python3 psp_out/check_retractions.py [--context N] [--min-len N]
"""
import os
import re
import sys

ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))

MARKERS = re.compile(
    r"RETRACT|retracted|retraction|superseded|SUPERSEDED|"
    r"\bboth are wrong\b|\bis wrong\b|\bwas wrong\b|\bwere wrong\b|"
    r"no longer (?:true|holds)|CORRECTION|"
    # supersession phrasings this tree actually uses, which do not contain the
    # word "retract" -- without these, a properly-superseded section reads as a
    # live claim and the tool cries wolf.
    r"original text is kept|budget artefact|section below concluded|"
    r"concluded that .* (?:was|were) ",
    re.I)

# quoted spans: "..." or `...`
QUOTED = re.compile(r'"([^"\n]{25,160})"|`([^`\n]{25,160})`')

# a digit, 0x-literal, underscore_identifier, or an ALLCAPS/CamelCase token
TECHNICAL = re.compile(r"0x[0-9a-fA-F]+|\d|_|\b[A-Z]{2,}\b|\b[A-Z][a-z]+[A-Z]\w*\b")


def md_files(root):
    for dirpath, dirnames, filenames in os.walk(root):
        dirnames[:] = [d for d in dirnames if d not in (".git", "__pycache__", ".venv")]
        for fn in filenames:
            if fn.endswith(".md"):
                yield os.path.join(dirpath, fn)


def load(path):
    with open(path, "r", errors="replace") as fh:
        return fh.read().splitlines()


def near_marker(lines, idx, context):
    lo = max(0, idx - context)
    hi = min(len(lines), idx + context + 1)
    return any(MARKERS.search(lines[i]) for i in range(lo, hi))


def main():
    context = 6
    min_len = 30
    if "--context" in sys.argv:
        context = int(sys.argv[sys.argv.index("--context") + 1])
    if "--min-len" in sys.argv:
        min_len = int(sys.argv[sys.argv.index("--min-len") + 1])

    files = sorted(md_files(ROOT))
    text = {p: load(p) for p in files}

    # 1. harvest claims quoted near a retraction marker
    claims = {}                                  # claim -> set of (file, line)
    for path, lines in text.items():
        for i, line in enumerate(lines):
            if not near_marker(lines, i, 2):
                continue
            for m in QUOTED.finditer(line):
                claim = (m.group(1) or m.group(2)).strip()
                if len(claim) < min_len:
                    continue
                # skip pure code/path/symbol tokens -- they recur legitimately
                if claim.count(" ") < 3:
                    continue
                # Require a technical anchor. Generic English ("the most
                # promising remaining lead") recurs across documents for
                # innocent reasons and is pure noise; a retracted *technical*
                # claim essentially always names something -- a number, a
                # register, an identifier, an ALLCAPS/CamelCase symbol.
                if not TECHNICAL.search(claim):
                    continue
                claims.setdefault(claim, set()).add((path, i + 1))

    print("harvested %d quoted claim(s) near retraction markers\n" % len(claims))

    # 2. find those claims restated elsewhere WITHOUT a nearby marker
    hits = []
    for claim, origins in sorted(claims.items()):
        for path, lines in text.items():
            for i, line in enumerate(lines):
                if claim not in line:
                    continue
                if (path, i + 1) in origins:
                    continue
                if near_marker(lines, i, context):
                    continue
                hits.append((claim, path, i + 1, line.strip()))

    if not hits:
        print("no un-propagated retracted claims found "
              "(context=%d lines, min-len=%d)" % (context, min_len))
        return 0

    print("CANDIDATE un-propagated claims (%d) -- review by hand:\n" % len(hits))
    for claim, path, ln, line in hits:
        rel = os.path.relpath(path, ROOT)
        print("  claim : %s" % (claim[:100] + ("..." if len(claim) > 100 else "")))
        print("  at    : %s:%d" % (rel, ln))
        print("  line  : %s" % line[:120])
        print()
    return 0


if __name__ == "__main__":
    sys.exit(main())