"""RUN-003 - Round 00's governance rules, measured on the corpus they govern. Round 00 fixes two rules every later document is bound by: sec. 25 canonical source: UTF-8; math only as $...$ and $$...$$; delimiters paired; no other math delimiters; no LaTeX turned into Unicode math; no unicode_escape round-trips; no secrets, keys or private data. sec. 21.6 claim ledger: every important result carries exactly one of ten statuses. The first is mechanical and is checked as a gate on the 42 canonical documents. The second is a census: which status words the corpus actually uses, where each first appears, and whether it is one of the ten. The census is written out as a status registry this tree fills in, round by round, with each word's definition when the round that introduces it is read. Checks (per canonical document; failures listed per document) G1 utf8 strict UTF-8 decode, no byte order mark G2 display-pairs an even number of $$ outside code G3 inline-pairs an even number of $ in every paragraph, outside code and $$ blocks G4 foreign-delims no \\( \\) \\[ \\] and no equation/align environments outside $$ G5 escapes no literal \\uXXXX outside code, no cp1252 mojibake G6 private no API keys, private keys, e-mail addresses, local paths or chat URLs Measured, not gated: M1 unicode-math Unicode math characters in prose (outside math and code) M2 status census see above Usage: python code/run003_round00_governance.py [--drill] [--blind CID] """ import argparse import collections import json import re from corpus import SOURCES, TREE, source_bytes, walk_sources LOG = TREE / "data" / "gate-logs" / "run003-round00-governance.json" REGISTRY = TREE / "data" / "STATUS_REGISTRY.v1.json" ALLOWED = ["PROVED-ANALYTIC", "VERIFIED-COMPUTATIONAL", "VERIFIED-THEOREM-APPLICATION", "DERIVED-CANDIDATE", "NUMERICAL-EVIDENCE", "CONDITIONAL", "COMPUTE-DEFERRED", "OPEN", "REJECTED", "CORRECTED"] GATE_WORDS = {"OPEN", "CLOSED"} FENCE = re.compile(r"^(```|~~~).*?^\1[^\n]*$", re.S | re.M) INLINE_CODE = re.compile(r"`[^`\n]*`") DISPLAY = re.compile(r"\$\$.*?\$\$", re.S) INLINE = re.compile(r"(?[^\n`*#|][^\n`]*?)[ \t]*[：:][ \t]*" r"(?:[\u4e00-\u9fff]{1,3}[ \t]*)?(?:`(?P[A-Z][A-Z0-9 \-/+]*[A-Z0-9])`" r"|(?P[A-Z][A-Z0-9 \-/+]*[A-Z0-9]))[ \t]*[.。,，;；]?[ \t]*$", re.M) PLAIN_LINE = re.compile(r"^([A-Z][A-Z0-9 \-/+]*[A-Z0-9])[.。]?[ \t]*$", re.M) PLAIN_HEADING = re.compile(r"^#{1,6}[ \t]+(\d+(?:\.\d+)*\.?[ \t]+)?(?:仍完全|仍為|仍然|仍)?[ \t]*" r"([A-Z][A-Z0-9 \-/+]*[A-Z0-9])[ \t]*$", re.M) SUMMARY_V5 = re.compile(r"^\*\*([^*\n]+?)[：:][ \t]*([^*\n]+?)\*\*[ \t]*$", re.M) def boxes(body): """(start, end, inner) of every \\boxed{...}, braces balanced to any depth""" out, i = [], 0 while True: i = body.find("\\boxed{", i) if i < 0: return out j, depth = i + len("\\boxed{"), 1 while j < len(body) and depth: if body[j - 1] != "\\": depth += {"{": 1, "}": -1}.get(body[j], 0) j += 1 out.append((i, j, body[i + len("\\boxed{"):j - 1])) i = j def render(part): """a set-off line as plain text, and the contents of its \\texttt{...} pieces""" s = part.replace("\n", " ") s = re.sub(r"\\begin\{[^{}]*\}|\\end\{[^{}]*\}|&", " ", s) s = re.sub(r"\\not\s*\\Rightarrow", " ⇏ ", s) s = re.sub(r"\\xRightarrow\{(?:[^{}]|\{[^{}]*\})*\}|\\Longrightarrow|\\Rightarrow|\\implies", " ⇒ ", s) s = re.sub(r"\\(?:longrightarrow|rightarrow|mapsto|to)(?![A-Za-z])", " → ", s) s = re.sub(r"\\(?:neq|ne)(?![A-Za-z])", " ≠ ", s) s = re.sub(r"\\gg(?![A-Za-z])", " ≫ ", s) s = re.sub(r"\\parallel(?![A-Za-z])", " ∥ ", s) s = re.sub(r"\\subseteq(?![A-Za-z])|\\subset(?![A-Za-z])", " ⊂ ", s) s = re.sub(r"\\(?:geq|ge)(?![A-Za-z])", "≥", s) s = re.sub(r"\\(?:leq|le)(?![A-Za-z])", "≤", s) s = re.sub(r"\\(?:qquad|quad)(?![A-Za-z])|\\[,;:! ]|~|\\rm(?![A-Za-z])", " ", s).replace("\\%", "%") explicit = set() while True: m = TEXTLIKE.search(s) if not m: break if m.group(1) == "texttt": explicit.add(m.group(2).strip().rstrip(".")) s = s[:m.start()] + m.group(2) + s[m.end():] return re.sub(r"\s+", " ", s.replace("\\_", "_")).strip(), explicit def is_status(phrase, known, explicit=()): """a capital run that the census counts as a status (see the v5 note above)""" if IDENT.match(phrase) or (NOT_STATUS.search(phrase) and not re.search(r"[ +/]", phrase)): return False if any(len(w) < 2 for w in re.split(r"[\s+/\-]+", phrase) if w): return False # U-L, C/G: the letters of a formula return (phrase in explicit or phrase in known or "-" in phrase or bool(re.search(r"[ +/]", phrase))) def end_status(t, explicit, known): """(claim, status) when a set-off line's last element is a status, else None""" t = re.sub(r"\s*(?:\([^()]*\)|（[^（）]*）)\s*[.。]?\s*$", "", t) t = re.sub(r"[\s.。,，;；]+$", "", t) m = RUN_AT_END.search(t) if not m: return None subject, status = t[:m.start()], m.group(1) while True: # 7856/7856 MPFR PASS: the backend's name is the claim's lead = re.match(rf"({WORD})\s+(?=\S)", status) if not lead or not NOT_STATUS.search(lead.group(1)): break subject, status = subject + lead.group(0), status[lead.end():] if not is_status(status, known, explicit): return None if any(op in subject for op in RULE_OPS): return None # an implication or a relation, not a verdict bare = subject.rstrip(" :：=") if bare.endswith("+"): return None # names joined by '+' if re.search(r"(?:^|[\s,])\d[\d.]*%?(?:\s+(?:fewer|more|raw))?$", bare): return None # a count: 2766 HARD, 32.73% fewer HARD runs = [r for r in CAPS_RUN.findall(subject) if is_status(r, known, explicit)] if runs and not re.sub(r"[\s,，;；→+/.]", "", CAPS_RUN.sub("", subject)): return None # a chain or a list of statuses subject = COPULA.sub("", bare).rstrip(" :：=,，;；") return subject, status def set_off(t, explicit, known): """the judgments on one set-off line: one, or one per part of a '+' conjunction""" parts = re.split(r"\s*\+\s*", t) if len(parts) > 1: each = [end_status(p, explicit, known) for p in parts] if all(e and e[0] for e in each): return each one = end_status(t, explicit, known) return [one] if one else [] def without_code(text): text = FENCE.sub(lambda m: "\n" * m.group(0).count("\n"), text) return INLINE_CODE.sub(lambda m: " " * len(m.group(0)), text) def without_math(text): text = DISPLAY.sub(lambda m: "\n" * m.group(0).count("\n"), text) return INLINE.sub(" ", text) def prose_only(text): return without_math(without_code(text)) def line_of(text, pos): return text.count("\n", 0, pos) + 1 # ---------------------------------------------------------------- the gate def g1_utf8(docs): out = [] for name, data in docs.items(): if data.startswith(b"\xef\xbb\xbf"): out.append(f"{name}: byte order mark") try: data.decode("utf-8", "strict") except UnicodeDecodeError as e: out.append(f"{name}: not UTF-8 at byte {e.start}") return out def decoded(docs): return {n: d.decode("utf-8", "replace") for n, d in docs.items()} def g2_display_pairs(docs): out = [] for name, text in decoded(docs).items(): n = without_code(text).count("$$") if n % 2: out.append(f"{name}: {n} display delimiters") return out def g3_inline_pairs(docs): out = [] for name, text in decoded(docs).items(): body = DISPLAY.sub(lambda m: "\n" * m.group(0).count("\n"), without_code(text)) # a stray $$ is G2's to report; this check counts single dollars only body = body.replace("$$", " ").replace("\\$", " ") pos = 0 for para in re.split(r"(\n\s*\n)", body): if para.count("$") % 2: out.append(f"{name}: odd $ count in paragraph at line {line_of(body, pos)}") pos += len(para) return out def g4_foreign_delims(docs): out = [] for name, text in decoded(docs).items(): body = without_code(text) for m in FOREIGN.finditer(body): out.append(f"{name}: {m.group(0)} at line {line_of(body, m.start())}") outside = DISPLAY.sub(lambda m: "\n" * m.group(0).count("\n"), body) for m in ENV.finditer(outside): out.append(f"{name}: \\begin{{{m.group(1)}}} outside $$ at line {line_of(outside, m.start())}") return out def g5_escapes(docs): out = [] for name, text in decoded(docs).items(): body = without_code(text) for m in UESC.finditer(body): out.append(f"{name}: literal {m.group(0)} at line {line_of(body, m.start())}") for m in MOJIBAKE.finditer(body): out.append(f"{name}: mojibake at line {line_of(body, m.start())}") return out def g6_private(docs): """Scans everything except math - code blocks included, since a path in a reproducibility snippet is as much a leak as one in prose. Math is excluded only because notation such as f:\\mathbb{R}\\to reads like a drive path.""" out = [] for name, text in decoded(docs).items(): body = without_math(text) for kind, rx in PRIVATE.items(): hits = rx.findall(body) if hits: # the tree records the kind and count, never the matched text out.append(f"{name}: {len(hits)} {kind}") return out CHECKS = {"G1": g1_utf8, "G2": g2_display_pairs, "G3": g3_inline_pairs, "G4": g4_foreign_delims, "G5": g5_escapes, "G6": g6_private} def run_checks(docs): return {cid: fn(docs) for cid, fn in CHECKS.items()} # ---------------------------------------------------------------- measurements def unicode_math(docs): out = {} for name, text in decoded(docs).items(): chars = UNICODE_MATH.findall(prose_only(text)) if chars: out[name] = {"count": len(chars), "distinct": "".join(sorted(set(chars)))} return out def round_no(name): m = re.search(r"Round_(\d+)", name) return int(m.group(1)) if m else None SINGLE_STATUS = {"OPEN", "CLOSED", "PASS", "FAIL", "PROVED", "CERTIFIED", "VERIFIED", "PARTIAL", "CANDIDATE", "DEFERRED", "CONDITIONAL", "REJECTED", "CORRECTED", "PENDING", "BLOCKED", "UNMEASURED", "YES", "NO"} ANSWER_WORDS = {"YES", "NO"} def plain_tex(s): """a boxed claim's name with its \\text{...} wrappers taken off""" return re.sub(r"\s+", " ", re.sub(r"\\text\{([^{}]*)\}", r"\1", s)).strip() def merge_registry(old, new): """census v3 into a registry already filled in: occurrences, counts, first rounds and classes come from the new census; every definition and review is kept""" st, changed = old["statuses"], [] for s, e in new.items(): if s not in st: st[s] = e changed.append(s) continue keep = {k: st[s][k] for k in ("definition", "reviews") if k in st[s]} fresh = {k: e[k] for k in ("first", "judgment_uses", "class", "occurrences")} if any(st[s].get(k) != v for k, v in fresh.items()): changed.append(s) st[s].update(fresh) st[s].update(keep) missing = sorted(set(st) - set(new)) return old, changed, missing def status_census(docs): """Status words by use and by position. Judgment positions: boxed \\text{X: S}; 'status:' / 狀態： / 判定： lines; bold summary lines **X: S**; and, from census v5, the forms described above CODE_LINE_STATUS_V5. Fenced code is skipped; inline code is kept, since status words are often written in backticks.""" uses = collections.Counter() judged = collections.Counter() first = {} judgments = [] order = lambda kv: (round_no(kv[0]) is None, round_no(kv[0]) or 0, kv[0]) docs_in_order = [] for name, text in sorted(decoded(docs).items(), key=order): r = round_no(name) where = f"R{r:02d}" if r is not None else name.split("_")[0] body = FENCE.sub(lambda m: "\n" * m.group(0).count("\n"), text) docs_in_order.append((where, body, *marked_forms(body))) # an unmarked capital word is a status if the corpus marks it as one somewhere known = set(ALLOWED) | GATE_WORDS | ANSWER_WORDS | SINGLE_STATUS known |= {status for _, _, found, _ in docs_in_order for _, _, status in found} for where, body, found, spans in docs_in_order: words = [t for t in STATUS_TOKEN.findall(body) if not NOT_STATUS.search(t)] words += re.findall(r"(?