1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
#!/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())
|
