#!/usr/bin/env python3
"""compare/build.py -- builds ../compare.html (#2 vs SOMDCv6 TM7) plus compare/TM7.html and compare/stats.json.

Every number on the page is computed here from the files:
  ours  = machines/<tm>/<tm>.v
  TM7   = vendor/busycoq/verify/SOMDCv6.v: the shared header (lines before `Module TM1.`) + the body of
          `Module TM7.` (the `Module TM7.` / `End TM7.` lines themselves are the "module wrapper", left out).
          rocq-scratch/TM7_toplevel.v is checked to be byte-identical to that, and the result is printed on the page.
Line diff: difflib.ndiff on trailing-space-trimmed lines, blank lines as junk, the TM string replaced by <TM>
in both files. ndiff pairs a removed and an added line as "changed" when they are similar (its 0.75 cutoff).
Counts are over non-blank lines.

Run:  [local working file] -B compare/build.py      (needs pygments)
"""
import difflib
import hashlib
import html
import json
import re
from collections import Counter, defaultdict
from pathlib import Path

from pygments.lexers import get_lexer_by_name
from pygments.token import Token

TM = "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"
ROOT = Path("[local working file]")
MD = ROOT / "machines" / TM
OURS = MD / f"{TM}.v"
VER = ROOT / "vendor/busycoq/verify"
SOMD = VER / "SOMDCv6.v"
TOP = MD / "rocq-scratch/TM7_toplevel.v"
CDIR = MD / "compare"
OUT = MD / "compare.html"
OUT_TM7 = CDIR / "TM7.html"
OUT_STATS = CDIR / "stats.json"

OURS_HREF = f"{TM}.v"            # rendered by tools/serve.py with #L-<n> anchors
TM7_HREF = "compare/TM7.html"    # our own rendered copy, anchors #L-<n> = SOMDCv6.v line numbers
SOMD_HREF = "../../vendor/busycoq/verify/SOMDCv6.v"
E = html.escape


def esc(s):
    return html.escape(str(s), quote=True)


def read_lines(p):
    return p.read_text(encoding="utf-8").splitlines()


def sha(p):
    return hashlib.sha256(p.read_bytes()).hexdigest()


# ---------------------------------------------------------------- sources
somd = read_lines(SOMD)
mods = []
for i, l in enumerate(somd):
    m = re.match(r"^Module (\w+)\.$", l)
    if m:
        j = next(k for k in range(i + 1, len(somd)) if somd[k] == f"End {m.group(1)}.")
        mods.append((m.group(1), i, j))
hdr_idx = list(range(0, mods[0][1]))  # SOMDCv6.v lines 1-17: everything before `Module TM1.`
MOD = {n: (s, e) for n, s, e in mods}
t7s, t7e = MOD["TM7"]
t8s, t8e = MOD["TM8"]
body7 = list(range(t7s + 1, t7e))
body8 = list(range(t8s + 1, t8e))
A = [(i + 1, somd[i]) for i in hdr_idx + body7]          # TM7 side: (SOMDCv6 line number, text)
B = [(i + 1, t) for i, t in enumerate(read_lines(OURS))]  # ours: (line number, text)
top_lines = read_lines(TOP)
TOP_FAITHFUL = top_lines == [t for _, t in A]
tm8_diff_lines = [(somd[a], somd[b]) for a, b in zip(body7, body8) if somd[a] != somd[b]]
assert len(body7) == len(body8)

TMSTR_RE = re.compile(r'TM_from_str "([^"]*)"')
tm_ours = TMSTR_RE.search("\n".join(t for _, t in B)).group(1)
tm_7 = TMSTR_RE.search("\n".join(somd[i] for i in body7)).group(1)
tm_8 = TMSTR_RE.search("\n".join(somd[i] for i in body8)).group(1)
assert tm_ours == TM


def norm(t):
    return TMSTR_RE.sub('TM_from_str "<TM>"', t.rstrip())


# ---------------------------------------------------------------- syntax classes per char
LEX = get_lexer_by_name("rocq", stripnl=False, stripall=False, ensurenl=True)


def tok_class(tt):
    if tt in Token.Comment:
        return "cm"
    if tt in Token.Keyword.Namespace:
        return "kv"
    if tt in Token.Keyword:
        return "kt"
    if tt in Token.Literal.String:
        return "st"
    if tt in Token.Literal.Number:
        return "nu"
    if tt in Token.Name.Builtin:
        return "nb"
    if tt in Token.Operator or tt in Token.Punctuation:
        return "op"
    return ""


def lex_lines(lines):
    text = "\n".join(lines) + "\n"
    chars = []
    for tt, v in LEX.get_tokens(text):
        c = tok_class(tt)
        chars.extend([c] * len(v))
    out, pos = [], 0
    for l in lines:
        out.append(chars[pos:pos + len(l)])
        pos += len(l) + 1
    rebuilt = "".join(v for _, v in LEX.get_tokens(text))
    assert rebuilt == text, "lexer changed the text"
    return out


tm7_show = [(i + 1, somd[i]) for i in hdr_idx] + [(i + 1, somd[i]) for i in range(t7s, t7e + 1)]
CLS7 = dict(zip([n for n, _ in tm7_show], lex_lines([t for _, t in tm7_show])))
CLSB = dict(zip([n for n, _ in B], lex_lines([t for _, t in B])))


def render(text, cls, flags=None):
    """text + per-char syntax classes (+ per-char diff flags) -> html"""
    if not text:
        return ""
    flags = flags or [""] * len(text)
    out, i = [], 0
    while i < len(text):
        j = i
        while j < len(text) and cls[j] == cls[i] and flags[j] == flags[i]:
            j += 1
        c = " ".join(x for x in (cls[i], flags[i]) if x)
        seg = E(text[i:j])
        out.append(f'<span class="{c}">{seg}</span>' if c else seg)
        i = j
    return "".join(out)


TOKEN_RE = re.compile(r"[A-Za-z0-9_']+|\s+|[^\sA-Za-z0-9_']")


TMSTR_TOK = re.compile(r"((?:[0-9\-][RL\-][A-Z\-]){2}(?:_(?:[0-9\-][RL\-][A-Z\-]){2})+)")


def tokens(s):
    """word / space / punctuation tokens; a machine string is split into its 3-char transitions."""
    out = []
    for n, part in enumerate(TMSTR_TOK.split(s)):
        if n % 2:
            out.extend(re.findall(r"_|.{3}", part))
        elif part:
            out.extend(TOKEN_RE.findall(part))
    assert "".join(out) == s
    return out


def intraline(a, b):
    """per-char flags for a changed line pair (token-level)."""
    ta, tb = tokens(a), tokens(b)
    fa, fb = [""] * len(a), [""] * len(b)
    pa = [0]
    for t in ta:
        pa.append(pa[-1] + len(t))
    pb = [0]
    for t in tb:
        pb.append(pb[-1] + len(t))
    for op, i1, i2, j1, j2 in difflib.SequenceMatcher(None, ta, tb, autojunk=False).get_opcodes():
        if op != "equal":
            for k in range(pa[i1], pa[i2]):
                fa[k] = "xd"
            for k in range(pb[j1], pb[j2]):
                fb[k] = "xi"
    return fa, fb


# ---------------------------------------------------------------- line diff
an = [norm(t) for _, t in A]
bn = [norm(t) for _, t in B]
nd = list(difflib.ndiff(an, bn, linejunk=lambda s: not s.strip()))
ops, i, j, k = [], 0, 0, 0
while k < len(nd):
    tg = nd[k][:2]
    if tg == "  ":
        ops.append(("eq", i, j)); i += 1; j += 1; k += 1
    elif tg == "- ":
        if k + 1 < len(nd) and nd[k + 1][:2] == "? ":
            assert nd[k + 2][:2] == "+ "
            ops.append(("chg", i, j)); i += 1; j += 1; k += 3
            if k < len(nd) and nd[k][:2] == "? ":
                k += 1
        elif k + 2 < len(nd) and nd[k + 1][:2] == "+ " and nd[k + 2][:2] == "? ":
            ops.append(("chg", i, j)); i += 1; j += 1; k += 3
        else:
            ops.append(("del", i, None)); i += 1; k += 1
    elif tg == "+ ":
        ops.append(("add", None, j)); j += 1; k += 1
    else:
        raise SystemExit(f"unexpected ndiff line {nd[k]!r}")
assert [x[1] for x in ops if x[1] is not None] == list(range(len(A)))
assert [x[2] for x in ops if x[2] is not None] == list(range(len(B)))


def nb(s):
    return bool(s.strip())


cnt = Counter()
cnt_all = Counter()
for op, i, j in ops:
    cnt_all[op] += 1
    if op == "eq" and nb(an[i]):
        cnt["identical"] += 1
    elif op == "chg":
        cnt["changed"] += 1
    elif op == "del" and nb(an[i]):
        cnt["removed"] += 1
    elif op == "add" and nb(bn[j]):
        cnt["added"] += 1
nbA = sum(nb(t) for t in an)
nbB = sum(nb(t) for t in bn)
assert cnt["identical"] + cnt["changed"] + cnt["removed"] == nbA
assert cnt["identical"] + cnt["changed"] + cnt["added"] == nbB
ws_only = sum(1 for op, i, j in ops if op == "chg" and re.sub(r"\s", "", an[i]) == re.sub(r"\s", "", bn[j]))
tm_line_pairs = [(i, j) for op, i, j in ops if op == "eq" and A[i][1] != B[j][1]]  # equal only after normalizing

# runs of equal op type (for the ribbon and for folding)
def oplab(op, i, j):
    return "tmn" if op == "eq" and A[i][1] != B[j][1] else op


runs = []
for idx, (op0, i, j) in enumerate(ops):
    op = oplab(op0, i, j)
    if runs and runs[-1]["op"] == op:
        r = runs[-1]
        r["n"] += 1
        r["end"] = idx
        if i is not None:
            r["a1"] = i
        if j is not None:
            r["b1"] = j
    else:
        runs.append({"op": op, "start": idx, "end": idx, "n": 1, "a0": i, "a1": i, "b0": j, "b1": j})
for r in runs:  # line positions for drawing: where the run sits in each file
    if r["a0"] is None:
        prev = [x for _, x, _ in ops[:r["start"]] if x is not None]
        r["a0"] = r["a1"] = (prev[-1] + 1) if prev else 0
        r["a_empty"] = True
    if r["b0"] is None:
        prev = [y for _, _, y in ops[:r["start"]] if y is not None]
        r["b0"] = r["b1"] = (prev[-1] + 1) if prev else 0
        r["b_empty"] = True

# ---------------------------------------------------------------- items
ITEM_RE = re.compile(r"^(Lemma|Theorem|Definition|Fixpoint|Inductive|Ltac|Notation)\s+(\"[^\"]*\"|[A-Za-z_][\w']*)")


def parse_items(L):
    starts, idx, in_cmt = [], 0, False
    while idx < len(L):
        t = L[idx][1]
        m = ITEM_RE.match(t)
        if t.startswith("(*"):
            starts.append([idx, "Comment", None])
            while "*)" not in L[idx][1]:
                idx += 1
        elif m:
            starts.append([idx, m.group(1), m.group(2)])
        elif re.match(r"^(From|Require)\b", t):
            if not (starts and starts[-1][1] == "Imports" and re.match(r"^(From|Require)\b", L[idx - 1][1])):
                starts.append([idx, "Imports", "imports"])
        elif re.match(r"^(Open|Close) Scope \w+\.", t):
            starts.append([idx, "Scope", t.strip().rstrip(".")])
        idx += 1
    items = []
    for n, (s, kind, name) in enumerate(starts):
        e = (starts[n + 1][0] if n + 1 < len(starts) else len(L)) - 1
        while e > s and not L[e][1].strip():
            e -= 1
        if kind == "Comment":
            first = L[s][1][2:].strip() or L[s + 1][1].strip()
            name = f"comment L{L[s][0]}"
            label = ("header comment" if s == 0 else "rule-table comment" if e == len(L) - 1
                     else first.replace("*)", "").strip(" -"))
        else:
            label = None
        items.append({"kind": kind, "name": name, "label": label, "s": s, "e": e,
                      "l0": L[s][0], "l1": L[e][0], "lines": [t for _, t in L[s:e + 1]]})
    return items


IA = parse_items(A)
IB = parse_items(B)
for II in (IA, IB):
    names = [x["name"] for x in II]
    assert len(names) == len(set(names)), [n for n, c in Counter(names).items() if c > 1]


def key_text(it):
    return "\n".join(l.rstrip() for l in it["lines"] if l.strip())


def nbl(it):
    return sum(1 for l in it["lines"] if l.strip())


KIND_GROUP = {"Lemma": "Lemma", "Theorem": "Lemma", "Definition": "Definition", "Fixpoint": "Definition",
              "Inductive": "Inductive", "Ltac": "Ltac", "Notation": "Notation"}

# role alignment (rocq-plan.md 1.2 / submission/proof.md 6): TM7 items whose job moved to a differently named item
ROLE = {"RIncs_nxt": "key"}
ATTACH = {"solve_v2": "RIncs_nxt", "solve_v1": "RIncs_nxt"}  # TM7 automation used only inside RIncs_nxt

NOTES = {
    "imports": "Individual62 (machine + segment machinery), Longitudinal, DivModCases, stdlib.",
    "esc": "proves a concrete segRLs / sideRLs goal by computation",
    "ec": "econstructor",
    "am": "segRLs over h^^(k*a+b) from two concrete facts (binary-counter digits)",
    "tm": "the only difference between the machines: A1 = 0RC (TM7) vs 0RF (ours)",
    "w1ld": "the word 1110 (the drain pass enters an L with a stray 1 in front); declared before Open Scope nat",
    "Inc": "new: one h pass = +1 on the 0/1 digits (little-endian binary, L skipped)",
    "RIncs": "the sweep as a relation. 2 L clauses gain an Inc premise; 2 new end clauses Z1, Z0",
    "z1_eq": "tape identity 1 100 0^inf = 110 0^inf, used by clause Z1",
    "z0_eq": "tape identity 1 000 0^inf = 100 0^inf, used by clause Z0",
    "Inc_spec": "new: Inc is what one h pass does on the tape (sideRLs tm h)",
    "seg_hx_ld": "new segment fact: the eater entering an L now emits h ++ h' ++ h^^(1+k)",
    "seg_h1_ld": "new segment fact: a drain pass entering an L (word 1110) emits h ++ h' ++ h^^(1+k)",
    "RIncs_spec": "soundness of RIncs. 8 bullets verbatim, the 2 L bullets rewritten, 2 bullets added (Z1, Z0)",
    "Inc_total": "new: Inc is total",
    "Inc_fun": "new: Inc is deterministic",
    "RIncs_eqk": "new: rewrite the pass count (k = k')",
    "inc_nil": "new Ltac: invert hypotheses Inc [] _",
    "RIncs_Inc": "new (proof.md Lemma A): one more pass after the k passes = +1 on the result",
    "RIncs_nxt_1": "the right end always succeeds in count mode",
    "End_1": "new: right-end cases; TM7 did r = [] inside RIncs_nxt by an inner induction on k",
    "End_x": "new: as End_1, ending in eater mode",
    "Inv": "new: the case condition of the domain lemma; with j = 0 it is TM7's RIncs_nxt condition",
    "key": "takes over RIncs_nxt's job (proof.md 3.3 calls it RIncs_nxt'): adds j pending +1 passes; induction on the derivation, not on r",
    "RIncs_nxt": "TM7's domain lemma; replaced by key (next row)",
    "solve_v2": "TM7 automation for RIncs_nxt's case list; ours writes key's cases out",
    "solve_v1": "TM7 automation for RIncs_nxt's case list; ours writes key's cases out",
    "domain": "new: key at j = 0, the form nonhalt needs",
    "lh": "left part of the boundary configuration",
    "S'": "the sweep boundary 0^inf 11 D> r 0^inf",
    "BigStep": "one sweep: S' r -->+ S' r'",
    "start": "new: c0 -->* S' [LD;D1] by esx (TM7 does its start, to S' [D1], inline inside nonhalt)",
    "nonhalt": "same statement; start S' [LD;D1], domain instead of RIncs_nxt, explicit witness",
    "Close Scope sym": "new; TM7 leaves the scope open",
}
NOTES.update({
    '"c -->* c\'"': "c reaches c' in zero or more steps of tm", '"c -->+ c\'"': "c reaches c' in one or more steps of tm",
    "ld": "digit L = 110", "d0": "digit 0 = 000", "d1": "digit 1 = 100",
    "hR": "a visit entering from the left in state B", "hR'": "a visit entering in state D with a 1 on its left",
    "hL": "a visit leaving to the left in state C",
    "h": "the drain-pass visit (in as B, out as C); in ours also the +1 pass",
    "h'": "the eater visit (in as D after a 1, out as C)",
    "RD": "the three digits", "H": "sweep modes: hx = eater, h1 = drain (count mode)",
    "toRC": "digit list -> right half of the tape", "toH'": "the extra cell in front of the digits (h1: a stray 1)",
    "toH": "the first visit of each mode", "cat3": "peel one 3-cell digit off the side",
    "tr1": "split h^^(1+k): first visit by computation", "wal": "k identical visits through a wall word",
    "tr2": "a leading sideRLs step", "Open Scope nat": "", "Open Scope sym": "",
})
for nm in ("inv_hx_ld", "inv_hx_d1", "inv_hx_d0", "inv_h1_ld", "inv_h1_d1", "inv_h1_d0", "inv_z1"):
    NOTES[nm] = "new: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)"
NOTES_CMT_OURS = {}  # filled from content below

A_by = {x["name"]: x for x in IA}
B_by = {x["name"]: x for x in IB}
rows = []
used_a = set()
for b in IB:
    a = A_by.get(b["name"])
    if b["name"] in ROLE.values():
        tm7name = next(k for k, v in ROLE.items() if v == b["name"])
        for att, host in ATTACH.items():
            if host == tm7name:
                rows.append({"tag": "tm7only", "a": A_by[att], "b": None, "group": "role"})
                used_a.add(att)
        rows.append({"tag": "tm7only", "a": A_by[tm7name], "b": None, "group": "role", "role_to": b["name"]})
        used_a.add(tm7name)
        rows.append({"tag": "new", "a": None, "b": b, "group": "role", "role_from": tm7name})
        continue
    if a:
        used_a.add(a["name"])
        rows.append({"tag": "identical" if key_text(a) == key_text(b) else "adapted", "a": a, "b": b})
    else:
        rows.append({"tag": "new", "a": None, "b": b})
leftover = [a for a in IA if a["name"] not in used_a]
for a in leftover:  # place after the row of the TM7 item just before it
    prev = IA[IA.index(a) - 1]["name"]
    pos = next(n for n, r in enumerate(rows) if r["a"] and r["a"]["name"] == prev)
    rows.insert(pos + 1, {"tag": "tm7only", "a": a, "b": None})
assert {r["a"]["name"] for r in rows if r["a"]} == {x["name"] for x in IA}
assert {r["b"]["name"] for r in rows if r["b"]} == {x["name"] for x in IB}

TAGS = ["identical", "adapted", "new", "tm7only"]
TAGNAME = {"identical": "identical", "adapted": "adapted", "new": "new", "tm7only": "TM7-only"}
KCOLS = ["Lemma", "Definition", "Inductive", "Ltac", "Notation", "other"]


def kgroup(r):
    it = r["b"] or r["a"]
    return KIND_GROUP.get(it["kind"], "other")


tagkind = defaultdict(Counter)
for r in rows:
    tagkind[r["tag"]][kgroup(r)] += 1
tag_tot = Counter(r["tag"] for r in rows)
lemmas_a = sum(1 for x in IA if x["kind"] in ("Lemma", "Theorem"))
lemmas_b = sum(1 for x in IB if x["kind"] in ("Lemma", "Theorem"))
named_a = sum(1 for x in IA if x["kind"] in KIND_GROUP)
named_b = sum(1 for x in IB if x["kind"] in KIND_GROUP)

# ---------------------------------------------------------------- clause / bullet level (RIncs, RIncs_spec)


def clauses(it):
    out, cur = [], None
    for l in it["lines"]:
        m = re.match(r"^\| (\w+)", l)
        if m:
            cur = [m.group(1), [l]]
            out.append(cur)
        elif cur and l.strip() not in (".", ""):
            cur[1].append(l)
    return [(n, "\n".join(x.rstrip() for x in ls if x.strip())) for n, ls in out]


def bullets(it):
    out, cur, inproof = [], None, False
    for l in it["lines"]:
        if l.strip() == "Proof.":
            inproof = True
            continue
        if not inproof or l.startswith("Qed"):
            continue
        if l.startswith("  - "):
            cur = [l]
            out.append(cur)
        elif cur is not None:
            cur.append(l)
    return ["\n".join(x.rstrip() for x in b if x.strip()) for b in out]


clA, clB = clauses(A_by["RIncs"]), clauses(B_by["RIncs"])
buA, buB = bullets(A_by["RIncs_spec"]), bullets(B_by["RIncs_spec"])
assert len(clA) == len(buA) and len(clB) == len(buB)
clA_d = dict(clA)
buA_d = {n: b for (n, _), b in zip(clA, buA)}
clause_rows = []
for (n, txt), bu in zip(clB, buB):
    clause_rows.append({"name": n,
                        "clause": "new" if n not in clA_d else ("identical" if clA_d[n] == txt else "adapted"),
                        "bullet": "new" if n not in buA_d else ("identical" if buA_d[n] == bu else "adapted")})
cl_cnt = Counter(c["clause"] for c in clause_rows)
bu_cnt = Counter(c["bullet"] for c in clause_rows)

# ---------------------------------------------------------------- key's repeated bullets (section 6)
kb = B_by["key"]
kbul = []
for n, l in enumerate(kb["lines"]):
    if l.startswith("  - "):
        kbul.append([l.strip(), []])
    elif kbul and l != "Qed.":
        kbul[-1][1].append(l)
same_body = defaultdict(list)
for h, body in kbul:
    same_body["\n".join(body)].append(h)
key_dupes = [(v, len([x for x in k.splitlines() if x.strip()])) for k, v in same_body.items() if len(v) > 1]
# bullets (not byte-identical) that end in the same lines: groups linked by a common tail of >= 3 lines


def _tail(b1, b2):
    s = 0
    while s < min(len(b1), len(b2)) and b1[-1 - s] == b2[-1 - s]:
        s += 1
    return s


_dupe_heads = {h for v, _ in key_dupes for h in v}
_kb = [(h, b) for h, b in kbul if h not in _dupe_heads]
_grp = {h: {h} for h, _ in _kb}
for x in range(len(_kb)):
    for y in range(x + 1, len(_kb)):
        if _tail(_kb[x][1], _kb[y][1]) >= 3:
            merged = _grp[_kb[x][0]] | _grp[_kb[y][0]]
            for h in merged:
                _grp[h] = merged
key_tail_dupes = []  # (heads in file order, shared tail lines, max differing head lines)
for g in {frozenset(v) for v in _grp.values() if len(v) > 1}:
    mem = [(h, b) for h, b in _kb if h in g]
    tail = min(_tail(mem[0][1], b) for _, b in mem[1:])
    head = max(len(b) - tail for _, b in mem)
    for _, b in mem:  # the differing lines at the top are the inversion step (checked, so the page text holds)
        assert all(re.match(r"\s*(destruct \(inv_|rewrite \(Inc_fun)", l) for l in b[:len(b) - tail]), b[:len(b) - tail]
    key_tail_dupes.append(([h for h, _ in mem], tail, head))
key_tail_dupes.sort(key=lambda t: kbul.index(next(x for x in kbul if x[0] == t[0][0])))


def bname(h):
    m = re.search(r"\(\* (\w+) \*\)", h)
    return m.group(1) if m else h


# ---------------------------------------------------------------- upstream conventions (section 6)
SKEL = ["RIncs_spec", "RIncs_nxt", "RIncs_nxt_1", "BigStep", "nonhalt"]
skel_counts = {}
for nm in SKEL:
    c = 0
    for mn, s, e in mods:
        if any(re.match(rf"^Lemma {re.escape(nm)}\b", somd[x]) for x in range(s, e)):
            c += 1
    skel_counts[nm] = c
somd_comments = sum(l.count("(*") for l in somd)
single = []
for f in sorted(VER.rglob("*.v")):
    if not re.match(r"^[0-9][RL][A-Z][0-9A-Z_\-]*\.v$", f.name):
        continue
    L = read_lines(f)
    txt = "\n".join(L)
    last_cmt = txt.rfind("(*")
    single.append({"name": f.name, "rel": str(f.relative_to(VER)), "lines": len(L), "comments": txt.count("(*"),
                   "module": any(re.match(r"^Module ", l) for l in L),
                   "fence": "```" in txt,
                   "ends_with_comment": last_cmt >= 0 and txt[last_cmt:].rstrip().endswith("*)") and
                   not re.search(r"\b(Lemma|Qed|Definition)\b", txt[txt.find("*)", last_cmt):])})
AUTH_RE = re.compile(r"\bauthors?\b|written by|claude|chatgpt|\bgpt\b|\bllm\b|ai-assisted", re.I)
all_v = sorted(VER.rglob("*.v"))  # subfolders (BigInt/, CounterClass1/) included
all_v_top = sorted(VER.glob("*.v"))
auth_hits = sorted({f.name for f in all_v if AUTH_RE.search(f.read_text(encoding="utf-8", errors="replace"))})
ours_comments = [x for x in IB if x["kind"] == "Comment"]
ours_cmt_lines = sum(x["l1"] - x["l0"] + 1 for x in ours_comments)
inline_cmt = sum(1 for _, t in B if "(*" in t and not t.startswith("(*"))
path_hits = [(n, m.group(0)) for n, t in B[:ours_comments[0]["l1"]]
             for m in re.finditer(r"(?<![\w.-])(vendor|machines|tools|rocq|scripts|reports)/[\w./\-]+", t)]
hdr_lines_n = len(hdr_idx)
hdr_text = [somd[i] for i in hdr_idx]
ours_hdr_at = next(n for n in range(len(B)) if [t for _, t in B[n:n + hdr_lines_n]] == hdr_text)
last_cmt = ours_comments[-1]
key_len = kb["l1"] - kb["l0"] + 1

# ---------------------------------------------------------------- stats
stats = {
    "tm_ours": tm_ours, "tm7": tm_7, "tm8": tm_8,
    "files": {"ours": str(OURS.relative_to(ROOT)), "somd": str(SOMD.relative_to(ROOT)),
              "ours_sha256": sha(OURS), "somd_sha256": sha(SOMD), "toplevel_sha256": sha(TOP)},
    "toplevel_faithful": TOP_FAITHFUL,
    "lines": {"ours": len(B), "tm7_module": t7e - t7s + 1, "tm7_module_range": [t7s + 1, t7e + 1],
              "tm7_body": len(body7), "header": hdr_lines_n, "tm7_plus_header": len(A),
              "ours_nonblank": nbB, "tm7_plus_header_nonblank": nbA, "somd_total": len(somd)},
    "diff_nonblank": dict(cnt), "diff_all_lines": dict(cnt_all), "whitespace_only_changes": ws_only,
    "tm_line_equal_after_norm": [(A[i][0], B[j][0]) for i, j in tm_line_pairs],
    "items": {"tag_totals": dict(tag_tot), "by_tag_kind": {t: dict(v) for t, v in tagkind.items()},
              "lemmas_tm7": lemmas_a, "lemmas_ours": lemmas_b, "named_tm7": named_a, "named_ours": named_b},
    "rincs_clauses": dict(cl_cnt), "rincs_spec_bullets": dict(bu_cnt),
    "tm8_vs_tm7_body_differing_lines": len(tm8_diff_lines),
    "modules": [(n, s + 1, e + 1) for n, s, e in mods], "skeleton_counts": skel_counts,
    "somd_comments": somd_comments, "single_machine_files": single,
    "ours_comments": [(x["l0"], x["l1"]) for x in ours_comments], "ours_inline_comments": inline_cmt,
    "header_path_mentions": path_hits, "ours_header_copy_at": B[ours_hdr_at][0],
    "authorship_search_hits": auth_hits, "verify_v_files": len(all_v), "verify_v_files_toplevel": len(all_v_top),
    "key_lines": [kb["l0"], kb["l1"]], "key_identical_bullets": key_dupes, "key_same_tail": key_tail_dupes,
}


def owner(II, idx):
    for it in II:
        if it["s"] <= idx <= it["e"]:
            return it["name"]
    return None


coincidental = []
for op, i, j in ops:
    if op == "eq" and an[i].strip():
        oa, ob = owner(IA, i), owner(IB, j)
        if oa != ob and ROLE.get(oa) != ob:
            coincidental.append((A[i][0], B[j][0], oa, ob, an[i].strip()))
stats["identical_across_items"] = coincidental
OUT_STATS.write_text(json.dumps(stats, indent=1, default=str) + "\n")

# ================================================================ HTML helpers
N = stats["lines"]
D = stats["diff_nonblank"]


def pct(a, b):
    return f"{100 * a / b:.0f}%"


def tag_chip(tag):
    return f'<span class="tag t-{tag}"><i></i>{TAGNAME[tag]}</span>'


def link_b(n, text=None):
    return f'<a class="ln" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{esc(OURS_HREF)}#L-{n}">{text or "L" + str(n)}</a>'


def link_a(n, text=None):
    return f'<a class="ln" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{TM7_HREF}#L-{n}">{text or "L" + str(n)}</a>'


def code_lines(L, CLS, l0, l1, numbered=True):
    out = []
    for n, t in L:
        if l0 <= n <= l1:
            ln = f'<span class="lno">{n}</span>' if numbered else ""
            out.append(ln + render(t, CLS[n]))
    return "\n".join(out)


def item_chars(it, L, CLS):
    text, cls = [], []
    first = True
    for n, t in L:
        if it["l0"] <= n <= it["l1"]:
            if not first:
                text.append("\n"); cls.append("")
            text.extend(t); cls.extend(CLS[n])
            first = False
    return "".join(text), cls


def word_diff(a_it, b_it):
    at, ac = item_chars(a_it, A, CLS7)
    bt, bc = item_chars(b_it, B, CLSB)
    ta, tb = tokens(at), tokens(bt)
    pa = [0]
    for t in ta:
        pa.append(pa[-1] + len(t))
    pb = [0]
    for t in tb:
        pb.append(pb[-1] + len(t))
    seq_t, seq_c, seq_f = [], [], []
    same = 0
    for op, i1, i2, j1, j2 in difflib.SequenceMatcher(None, ta, tb, autojunk=False).get_opcodes():
        if op == "equal":
            same += sum(1 for t in ta[i1:i2] if t.strip())
            for k in range(pb[j1], pb[j2]):
                seq_t.append(bt[k]); seq_c.append(bc[k]); seq_f.append("")
        else:
            for k in range(pa[i1], pa[i2]):
                seq_t.append(at[k]); seq_c.append(ac[k]); seq_f.append("xd")
            for k in range(pb[j1], pb[j2]):
                seq_t.append(bt[k]); seq_c.append(bc[k]); seq_f.append("xi")
    na = sum(1 for t in ta if t.strip())
    nbt = sum(1 for t in tb if t.strip())
    return render("".join(seq_t), seq_c, seq_f), same, na, nbt


def disp_name(it):
    if it["kind"] == "Comment":
        lab = it["label"]
        return f'<span class="cmt">(* {E(lab[:36])}{"…" if len(lab) > 36 else ""} *)</span>'
    return f"<code>{E(it['name'])}</code>"


def kind_label(it):
    return {"Imports": "imports", "Scope": "scope", "Comment": "comment"}.get(it["kind"], it["kind"])


def span_txt(it):
    n = nbl(it)
    return f'{n} line{"s" if n != 1 else ""}'


# ================================================================ section 1: machines
def tm_cells(s):
    st = s.split("_")
    return {(chr(65 + q), sym): st[q][3 * sym:3 * sym + 3] for q in range(6) for sym in (0, 1)}


C_OURS, C_7, C_8 = tm_cells(tm_ours), tm_cells(tm_7), tm_cells(tm_8)
diff_7 = [k for k in C_OURS if C_OURS[k] != C_7[k]]
diff_8 = [k for k in C_OURS if C_OURS[k] != C_8[k]]
diff_78 = [k for k in C_7 if C_7[k] != C_8[k]]
assert diff_7 == [("A", 1)] and diff_8 == [("A", 1)] and diff_78 == [("A", 1)]


def tm_table(title, sub, cells, cls):
    rows_h = []
    for q in "ABCDEF":
        tds = []
        for sym in (0, 1):
            c = cells[(q, sym)]
            klass = []
            if (q, sym) == ("A", 1):
                klass.append("a1")
            if cells is not C_OURS and c != C_OURS[(q, sym)]:
                klass.append("neq")
            tds.append(f'<td class="{" ".join(klass)}">{"halt" if c == "---" else E(c)}</td>')
        rows_h.append(f"<tr><th>{q}</th>{''.join(tds)}</tr>")
    return (f'<figure class="tmt {cls}"><figcaption><b>{title}</b><span>{sub}</span></figcaption>'
            f'<table class="tt"><thead><tr><th></th><th>read 0</th><th>read 1</th></tr></thead>'
            f'<tbody>{"".join(rows_h)}</tbody></table></figure>')


def tm_str_mark(s):
    return f"<code>{E(s[:3])}<mark>{E(s[3:6])}</mark>{E(s[6:])}</code>"


def say(entry):
    w, mv, st = entry[0], {"R": "right", "L": "left"}[entry[1]], entry[2]
    return f"write {w}, move {mv}, go to {st}"


S1 = f"""
<div class="tmrow">
{tm_table("#2 (ours)", "the holdout we proved", C_OURS, "ours")}
{tm_table("TM7", "SOMDCv6.v, our template", C_7, "")}
{tm_table("TM8", "SOMDCv6.v, same proof text as TM7", C_8, "")}
<div class="tmside">
<p class="k">Machine strings (A1 marked)</p>
<p>{tm_str_mark(tm_ours)} <span class="muted">#2</span></p>
<p>{tm_str_mark(tm_7)} <span class="muted">TM7</span></p>
<p>{tm_str_mark(tm_8)} <span class="muted">TM8</span></p>
<p class="k">A1 = state A reading a 1</p>
<ul class="tight">
<li>#2 <code>{C_OURS[("A", 1)]}</code>: {say(C_OURS[("A", 1)])}</li>
<li>TM7 <code>{C_7[("A", 1)]}</code>: {say(C_7[("A", 1)])}</li>
<li>TM8 <code>{C_8[("A", 1)]}</code>: {say(C_8[("A", 1)])}</li>
</ul>
<p class="k">Cells that differ (of 12)</p>
<ul class="tight">
<li>#2 vs TM7: {len(diff_7)} (A1) · #2 vs TM8: {len(diff_8)} (A1) · TM7 vs TM8: {len(diff_78)} (A1)</li>
<li>TM8's module body differs from TM7's in {len(tm8_diff_lines)} of {len(body7)} lines: the <code>tm</code> line. So everything below holds for TM8 too, except the TM string.</li>
</ul>
<p><a class="btn" href="/busy-beaver/machines/tools/explorer/index.html#preset=p2-vs-tm7">Open #2 vs TM7 in the explorer &rarr;</a>
<span class="muted small">preset <code>p2-vs-tm7</code>: both machines from the same start; the dashed line is A1's first firing. <code>d</code> = diff view.</span></p>
</div>
</div>"""

# ================================================================ section 2: similarity
mx = max(nbA, nbB)


SHORT = {"identical": "identical", "adapted": "changed", "tm7only": "TM7 only", "new": "ours only"}


def bar(label, total, segs, total_lines):
    parts = []
    for name, n, tag in segs:
        w = 100 * n / total
        inside = f"{n} {SHORT[tag]}" if w > 14 else (str(n) if w > 4 else "")
        parts.append(f'<div class="seg s-{tag}" style="flex:{n} 0 0" title="{n} {name} lines">'
                     f'<span>{inside}</span></div>')
    legend = " ".join(f'<span class="lg"><i class="s-{tag}"></i><b>{n}</b> {name}</span>' for name, n, tag in segs)
    return (f'<div class="barrow"><div class="barlab"><b>{label}</b><span>{total} non-blank of {total_lines} lines</span></div>'
            f'<div class="barbox"><div class="bar" style="width:{100 * total / mx:.2f}%">{"".join(parts)}</div>'
            f'<div class="barleg">{legend}</div></div></div>')


BAR_A = bar("TM7 + shared header", nbA, [("identical", D["identical"], "identical"), ("changed", D["changed"], "adapted"),
                                          ("TM7 only (removed)", D["removed"], "tm7only")], len(A))
BAR_B = bar("#2 (ours)", nbB, [("identical", D["identical"], "identical"), ("changed", D["changed"], "adapted"),
                               ("ours only (added)", D["added"], "new")], len(B))


# ribbon map: where the identical runs sit in each file (all lines, same scale)
def ribbon():
    W = 1000.0
    s = W / max(len(A), len(B))
    ya0, ya1, yb0, yb1 = 26, 40, 112, 126
    el = []
    for ri, r in enumerate(runs):
        op = r["op"]
        a0, a1, b0, b1 = r["a0"], r["a1"] + (0 if r.get("a_empty") else 1), r["b0"], r["b1"] + (0 if r.get("b_empty") else 1)
        xa0, xa1, xb0, xb1 = a0 * s, a1 * s, b0 * s, b1 * s
        la = f"TM7 L{A[r['a0']][0]}–{A[r['a1']][0]}" if not r.get("a_empty") else ""
        lb = f"ours L{B[r['b0']][0]}–{B[r['b1']][0]}" if not r.get("b_empty") else ""
        what = {"eq": "identical", "chg": "changed", "del": "TM7 only", "add": "ours only",
                "tmn": "equal after replacing the TM string by <TM> (the strings differ in A1)"}[op]
        tip = f"{r['n']} line{'s' if r['n'] > 1 else ''} {what}: " + " ↔ ".join(x for x in (la, lb) if x)
        cls = {"eq": "identical", "chg": "adapted", "del": "tm7only", "add": "new", "tmn": "tmn"}[op]
        g = [f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#r</span><span class="si">{ri}" data-tip="{esc(tip)}"><title>{esc(tip)}</title>']
        if op in ("eq", "chg", "tmn"):
            g.append(f'<polygon class="band b-{cls}" points="{xa0:.1f},{ya1} {xa1:.1f},{ya1} {xb1:.1f},{yb0} {xb0:.1f},{yb0}"/>')
        if not r.get("a_empty"):
            g.append(f'<rect class="f-{cls}" x="{xa0:.1f}" y="{ya0}" width="{max(xa1 - xa0, 0.8):.1f}" height="{ya1 - ya0}"/>')
        if not r.get("b_empty"):
            g.append(f'<rect class="f-{cls}" x="{xb0:.1f}" y="{yb0}" width="{max(xb1 - xb0, 0.8):.1f}" height="{yb1 - yb0}"/>')
        g.append("</a>")
        el.append("".join(g))
    txt = (f'<text x="0" y="18" class="rl">TM7 + header: {len(A)} lines (SOMDCv6.v 1–{hdr_lines_n}, {t7s + 2}–{t7e})</text>'
           f'<text x="0" y="142" class="rl">#2 (ours): {len(B)} lines</text>'
           f'<text x="{len(A) * s:.1f}" y="18" class="rl" text-anchor="end">L{A[-1][0]}</text>'
           f'<text x="{W}" y="142" class="rl" text-anchor="end">L{len(B)}</text>')
    return (f'<svg class="ribbon" viewBox="0 0 {W:.0f} 148" role="img" aria-label="Positions of identical, changed and added runs">'
            f'{"".join(el)}{txt}</svg>')


def tagkind_table():
    head = "".join(f"<th>{k}</th>" for k in KCOLS)
    body = []
    for t in TAGS:
        cells = "".join(f'<td>{tagkind[t][k] or "<span class=muted>·</span>"}</td>' for k in KCOLS)
        body.append(f"<tr><th>{tag_chip(t)}</th>{cells}<td><b>{tag_tot[t]}</b></td></tr>")
    tot = "".join(f"<td>{sum(tagkind[t][k] for t in TAGS)}</td>" for k in KCOLS)
    body.append(f'<tr class="tot"><th>rows</th>{tot}<td><b>{len(rows)}</b></td></tr>')
    return f'<div class="hscroll"><table class="mx"><thead><tr><th></th>{head}<th>all</th></tr></thead><tbody>{"".join(body)}</tbody></table></div>'


kept = D["identical"]
FIXPOINTS = ", ".join(f"<code>{E(n)}</code>" for n in sorted({x["name"] for x in IA + IB if x["kind"] == "Fixpoint"}))
S2 = f"""
<div class="tiles">
<div class="tile"><div class="big">{N['ours']}</div><div class="lab">lines in ours<br><span class="muted">{nbB} non-blank</span></div></div>
<div class="tile"><div class="big">{N['tm7_module']}</div><div class="lab">lines in Module TM7<br><span class="muted">SOMDCv6.v {N['tm7_module_range'][0]}–{N['tm7_module_range'][1]}</span></div></div>
<div class="tile"><div class="big">{N['tm7_plus_header']}</div><div class="lab">TM7 body + shared header<br><span class="muted">{nbA} non-blank; what we diff against</span></div></div>
<div class="tile hl"><div class="big">{kept}<small>/{nbA}</small></div><div class="lab">TM7 lines kept verbatim ({pct(kept, nbA)})<br><span class="muted">they are {pct(kept, nbB)} of ours</span></div></div>
<div class="tile"><div class="big">{N['ours'] / N['tm7_plus_header']:.1f}&times;</div><div class="lab">longer than TM7 + header<br><span class="muted">{N['ours'] / N['tm7_module']:.1f}&times; the module alone</span></div></div>
</div>
<h3>Non-blank lines by diff status <span class="muted">(same scale)</span></h3>
{BAR_A}
{BAR_B}
<p class="foot">{len(coincidental)} of the {kept} identical lines are a {" and a ".join(f"<code>{E(c[4])}</code>" for c in coincidental)} that difflib matched across different lemmas ({"; ".join(f"TM7 {c[2]} L{c[0]} ↔ ours {c[3]} L{c[1]}" for c in coincidental)}).
The <code>Definition tm</code> line counts as identical because the TM string is replaced by <code>&lt;TM&gt;</code> before diffing (section 1 shows the real difference).
{ws_only} of the {D['changed']} changed lines differ only in whitespace.</p>
<h3>Where the identical lines are <span class="muted">(each file drawn to the same scale, all lines; hover or click a band)</span></h3>
{ribbon()}
<p class="readout" id="ribbon-readout">Hover a band: grey = identical run, amber = changed, red = TM7 only, green = ours only. Click to jump to it in section 4.</p>
<div class="two">
<div><h3>Items by tag and kind</h3>{tagkind_table()}
<p class="foot">"other" = imports, <code>Open/Close Scope</code> and comments; Definition includes Fixpoint ({FIXPOINTS}). Lemmas: TM7 {lemmas_a}, ours {lemmas_b}. Named items (Lemma, Definition, Fixpoint, Inductive, Ltac, Notation): TM7 {named_a}, ours {named_b}.</p></div>
<div><h3>How the numbers are computed</h3>
<ul class="tight small">
<li>TM7 side = SOMDCv6.v lines 1–{hdr_lines_n} (shared header) + {t7s + 2}–{t7e} (Module TM7 body). The <code>Module TM7.</code> / <code>End TM7.</code> lines are left out.</li>
<li>That is byte-identical to <code>rocq-scratch/TM7_toplevel.v</code>: <b>{"yes" if TOP_FAITHFUL else "NO"}</b> (sha256 <code>{stats['files']['toplevel_sha256'][:12]}…</code>).</li>
<li>Line diff: Python <code>difflib.ndiff</code> on lines with trailing spaces trimmed, blank lines treated as junk, and the TM string replaced by <code>&lt;TM&gt;</code> in both files. A removed line and an added line count as one <i>changed</i> line when ndiff pairs them (similarity cutoff 0.75).</li>
<li>Items: every top-level sentence starting with Lemma / Definition / Fixpoint / Inductive / Ltac / Notation, plus imports, scopes and comments. Paired by name; <code>RIncs_nxt</code> is paired by role with <code>key</code>. <i>identical</i> = the same text (trailing spaces and blank lines ignored, TM string <i>not</i> normalized, so <code>tm</code> is <i>adapted</i>).</li>
<li>Built by <code>compare/build.py</code>; all numbers also in <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/compare/stats.json">compare/stats.json</a>.</li>
</ul></div>
</div>"""

# ================================================================ section 3: lemma table
def run_of_b(jidx):
    """index of the section-4 run that holds line index jidx of ours (its first row carries id r<index>)"""
    return next(ri for ri, r in enumerate(runs) if not r.get("b_empty") and r["b0"] <= jidx <= r["b1"])


ROW_HTML = []
for r in rows:
    a, b, tag = r["a"], r["b"], r["tag"]
    it = b or a
    acell = (f'{disp_name(a)} {link_a(a["l0"])} <span class="muted">{span_txt(a)}</span>' if a else
             '<span class="muted">—</span>')
    bcell = (f'{disp_name(b)} {link_b(b["l0"])} <span class="muted">{span_txt(b)}</span>' if b else
             '<span class="muted">—</span>')
    note = NOTES.get(it["name"], "")
    if it["kind"] == "Comment":
        note = "comment (ours only)"
    if r.get("role_to"):
        note = NOTES["RIncs_nxt"]
    if tag == "identical":
        body = (f'<p class="bh">Identical text in both files: TM7 {link_a(a["l0"], f"L{a["l0"]}–{a["l1"]}")}, '
                f'ours {link_b(b["l0"], f"L{b["l0"]}–{b["l1"]}")}.</p>'
                f'<pre class="code">{code_lines(B, CLSB, b["l0"], b["l1"])}</pre>')
    elif tag == "adapted":
        wd, same, na, nbt = word_diff(a, b)
        body = (f'<p class="bh">Word diff, TM7 {link_a(a["l0"], f"L{a["l0"]}–{a["l1"]}")} &rarr; ours '
                f'{link_b(b["l0"], f"L{b["l0"]}–{b["l1"]}")}: {same} of TM7\'s {na} tokens kept, ours has {nbt}. '
                f'<del class="xd">struck red</del> = TM7 only, <ins class="xi">green</ins> = ours only. '
                f'<a class="jump" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#r</span><span class="si">{run_of_b(b["s"])}">Line by line in section 4 &darr;</a></p>'
                f'<pre class="code wd">{wd}</pre>')
    elif tag == "new":
        body = f'<pre class="code">{code_lines(B, CLSB, b["l0"], b["l1"])}</pre>'
        if r.get("role_from"):
            ra = A_by[r["role_from"]]
            stA = ra["lines"][:next(n for n, l in enumerate(ra["lines"]) if l.strip() == "Proof.")]
            stB = b["lines"][:next(n for n, l in enumerate(b["lines"]) if l.strip() == "Proof.")]
            inv = B_by["Inv"]
            body = (f'<p class="bh">Statements side by side: TM7\'s <code>RIncs_nxt</code> (with its case condition inline) '
                    f'vs ours <code>key</code> (case condition in <code>Inv</code>). With <code>j = 0</code>, <code>Inv</code> '
                    f'is exactly TM7\'s condition.</p><div class="pair">'
                    f'<pre class="code">{code_lines(A, CLS7, ra["l0"], ra["l0"] + len(stA) - 1)}</pre>'
                    f'<pre class="code">{code_lines(B, CLSB, inv["l0"], inv["l1"])}\n\n{code_lines(B, CLSB, b["l0"], b["l0"] + len(stB) - 1)}</pre>'
                    f'</div><p class="bh">Full text of <code>key</code> ({span_txt(b)}):</p>' + body)
    else:
        body = f'<pre class="code">{code_lines(A, CLS7, a["l0"], a["l1"])}</pre>'
    grp = ' role' if r.get("group") == "role" else ""
    ROW_HTML.append(
        f'<details class="it t-{tag}{grp}" data-tag="{tag}"><summary>'
        f'<span class="c-tag">{tag_chip(tag)}</span><span class="c-kind">{kind_label(it)}</span>'
        f'<span class="c-a">{acell}</span><span class="c-b">{bcell}</span><span class="c-note">{E(note)}</span>'
        f'</summary><div class="ib">{body}</div></details>')

FILTERS = "".join(
    f'<button class="flt{" on" if t == "all" else ""}" data-f="{t}">{"all" if t == "all" else TAGNAME[t]} '
    f'<b>{len(rows) if t == "all" else tag_tot[t]}</b></button>' for t in ["all"] + TAGS)
S3 = f"""
<div class="ctl">{FILTERS}<span class="sp"></span><button class="act" data-act="open-adapted">Open all adapted</button><button class="act" data-act="close-all">Close all</button></div>
<div class="ithead"><span>tag</span><span>kind</span><span>TM7 (SOMDCv6.v line)</span><span>ours (.v line)</span><span>what it is / what changed</span></div>
<div class="items">{"".join(ROW_HTML)}</div>
<p class="foot">Rows follow our file's order; TM7-only rows sit next to the row that took over their job. The shaded group (<code>solve_v2</code>, <code>solve_v1</code>, <code>RIncs_nxt</code> &rarr; <code>key</code>) is the one role pairing: TM7's domain lemma and its automation, replaced by ours. "<i>n</i> lines" counts non-blank lines. Line links open the highlighted files (ours via the local server, TM7 in <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{TM7_HREF}">compare/TM7.html</a> with SOMDCv6.v line numbers).</p>
"""

# ================================================================ section 4: side-by-side
CTX = 3
ops_rows = []  # (run index or None, html)


def row_html(op, i, j, rid=None, lab=None):
    if op == "eq" and i is not None and A[i][1] != B[j][1]:
        fa, fb = intraline(A[i][1], B[j][1])
        klass, mark = "eq tmn", "≈"
    elif op == "chg":
        fa, fb = intraline(A[i][1], B[j][1])
        klass, mark = "chg", "~"
    else:
        fa = fb = None
        klass, mark = op, {"eq": "", "del": "−", "add": "+"}[op]
    if i is not None:
        n = A[i][0]
        la = f'<td class="ln"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{TM7_HREF}#L-{n}">{n}</a></td><td class="cd">{render(A[i][1], CLS7[n], fa)}</td>'
    else:
        la = '<td class="ln"></td><td class="cd empty"></td>'
    if j is not None:
        n = B[j][0]
        lb = f'<td class="ln"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{esc(OURS_HREF)}#L-{n}">{n}</a></td><td class="cd">{render(B[j][1], CLSB[n], fb)}</td>'
    else:
        lb = '<td class="ln"></td><td class="cd empty"></td>'
    idattr = f' id="r{rid}"' if rid is not None else ""
    chg = ' data-chg="1"' if (rid is not None and (lab or op) != "eq") else ""
    tip = ' title="equal after replacing the TM string by &lt;TM&gt;; the strings differ in A1"' if "tmn" in klass else ""
    return f'<tr class="{klass}"{idattr}{chg}{tip}>{la}<td class="mk">{mark}</td>{lb}</tr>'


SBS = []
folds = 0
for ri, r in enumerate(runs):
    seg = ops[r["start"]:r["end"] + 1]
    rws = [row_html(op, i, j, ri if n == 0 else None, r["op"]) for n, (op, i, j) in enumerate(seg)]
    if r["op"] == "eq" and len(rws) > 2 * CTX + 3:
        hid = len(rws) - 2 * CTX
        a_from, a_to = A[seg[CTX][1]][0], A[seg[-CTX - 1][1]][0]
        b_from, b_to = B[seg[CTX][2]][0], B[seg[-CTX - 1][2]][0]
        SBS.append(f'<tbody>{"".join(rws[:CTX])}</tbody>')
        SBS.append(f'<tbody class="foldbar"><tr><td colspan="5"><button class="fold" aria-expanded="false">'
                   f'<span class="fx">▸</span> {hid} identical lines '
                   f'<span class="muted">(TM7 {a_from}–{a_to} · ours {b_from}–{b_to})</span></button></td></tr></tbody>')
        SBS.append(f'<tbody class="fold" hidden>{"".join(rws[CTX:-CTX])}</tbody>')
        SBS.append(f'<tbody>{"".join(rws[-CTX:])}</tbody>')
        folds += 1
    else:
        SBS.append(f'<tbody>{"".join(rws)}</tbody>')

S4 = f"""
<div class="ctl sticky">
<button class="act" data-act="expand">Show all identical lines</button>
<button class="act" data-act="collapse">Fold identical runs</button>
<button class="act" data-act="next">Next change &darr;</button>
<button class="act" data-act="prev">&uarr; Previous</button>
<span class="sp"></span>
<span class="lg"><i class="s-adapted"></i>changed (~)</span><span class="lg"><i class="s-tm7only"></i>TM7 only (−)</span>
<span class="lg"><i class="s-new"></i>ours only (+)</span><span class="lg"><i class="s-tmn"></i>equal after normalizing the TM string (≈)</span>
</div>
<div class="sbswrap"><table class="sbs">
<colgroup><col class="cl"><col class="cc"><col class="cm"><col class="cl"><col class="cc"></colgroup>
<thead><tr><th colspan="2">TM7 · SOMDCv6.v lines 1–{hdr_lines_n} + {t7s + 2}–{t7e} (<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{TM7_HREF}">highlighted copy</a>)</th><th></th>
<th colspan="2">#2 (ours) · <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{esc(OURS_HREF)}">{E(TM)}.v</a></th></tr></thead>
{"".join(SBS)}
</table></div>
<p class="foot">{folds} identical runs longer than {2 * CTX + 3} lines are folded to {CTX} lines of context on each side. Inside changed lines the differing tokens are marked. Line numbers link to the highlighted files.</p>
"""

# ================================================================ section 5: structure diagram
NOT_A = ['"c -->* c\'"', '"c -->+ c\'"', "ld", "d0", "d1", "hR", "hR'", "hL", "h", "h'", "RD", "H", "toRC", "toH'", "toH"]
HDR = ["imports", "esc", "ec", "am"]
TAC = ["cat3", "tr1", "wal", "tr2"]
INV_H = [x["name"] for x in IB if x["name"].startswith("inv_")]
cmt_b = [x["name"] for x in IB if x["kind"] == "Comment"]  # comments in file order
BLOCKS_A = [
    ("hdr", "shared header", HDR), ("tm", "tm (A1 = 0RC)", ["tm"]),
    ("not", "notations, digits, toRC, toH", NOT_A), ("rincs", f"RIncs: {len(clA)} clauses", ["RIncs"]),
    ("tac", "cat3, tr1, wal, tr2", TAC), ("spec", "RIncs_spec", ["RIncs_spec"]), ("nxt1", "RIncs_nxt_1", ["RIncs_nxt_1"]),
    ("dom", "solve_v2, solve_v1, RIncs_nxt", ["solve_v2", "solve_v1", "RIncs_nxt"]),
    ("big", "lh, S', BigStep", ["lh", "S'", "BigStep"]), ("nh", "nonhalt", ["nonhalt"]),
]
BLOCKS_B = [
    ("cmt0", "header comment", [cmt_b[0]]), ("hdr", "shared header", HDR), ("tm", "tm (A1 = 0RF)", ["tm"]),
    ("not", "notations, digits, toRC, toH, + w1ld", NOT_A[:5] + ["w1ld"] + NOT_A[5:]),
    ("inc", "Inc", [cmt_b[1], "Inc"]), ("rincs", f"RIncs: {len(clB)} clauses", ["RIncs"]),
    ("tac", "cat3, tr1, wal, tr2", TAC), ("zeq", "z1_eq, z0_eq", ["z1_eq", "z0_eq"]),
    ("seg", "Inc_spec, seg_hx_ld, seg_h1_ld", ["Inc_spec", "seg_hx_ld", "seg_h1_ld"]),
    ("spec", "RIncs_spec", ["RIncs_spec"]),
    ("incl", "Inc_total, Inc_fun, RIncs_eqk, inc_nil, RIncs_Inc", [cmt_b[2], "Inc_total", "Inc_fun", "RIncs_eqk", "inc_nil", cmt_b[3], "RIncs_Inc"]),
    ("nxt1", "RIncs_nxt_1", ["RIncs_nxt_1"]), ("end", "End_1, End_x", ["End_1", "End_x"]),
    ("inv", f"inv_* ({len(INV_H)} inversion helpers)", [cmt_b[4]] + INV_H),
    ("dom", "Inv + key", [cmt_b[5], "Inv", "key"]), ("domw", "domain", ["domain"]),
    ("big", "lh, S', BigStep", ["lh", "S'", "BigStep"]), ("start", "start", ["start"]), ("nh", "nonhalt", ["nonhalt"]),
    ("cmt1", "rule-table comment", [cmt_b[6]]),
]
for BL, II in ((BLOCKS_A, IA), (BLOCKS_B, IB)):
    have = [n for _, _, ns in BL for n in ns]
    names = {x["name"] for x in II}
    assert set(have) <= names, set(have) - names
    missing = [x["name"] for x in II if x["name"] not in have and x["kind"] != "Scope"]
    assert not missing, missing
opA = {i: op for op, i, j in ops if i is not None}
opB = {j: op for op, i, j in ops if j is not None}


def block_stats(BL, II, L, opmap, which):
    by = {x["name"]: x for x in II}
    out = []
    for key_, label, ns in BL:
        c = Counter()
        for n in ns:
            it = by[n]
            for idx in range(it["s"], it["e"] + 1):
                if L[idx][1].strip():
                    o = opmap[idx]
                    if o == "eq" and idx in tmn_idx[which]:
                        c["tmn"] += 1
                    else:
                        c[{"eq": "identical", "chg": "adapted", "del": "tm7only", "add": "new"}[o]] += 1
        out.append({"key": key_, "label": label, "c": c, "n": sum(c.values()),
                    "l0": by[ns[0]]["l0"], "l1": by[ns[-1]]["l1"]})
    return out


tmn_idx = {"a": {i for i, j in tm_line_pairs}, "b": {j for i, j in tm_line_pairs}}
BSA = block_stats(BLOCKS_A, IA, A, opA, "a")
BSB = block_stats(BLOCKS_B, IB, B, opB, "b")


def structure_svg():
    PX, MINH, GAP = 1.0, 18, 5
    XA, XB, BW = 350, 820, 230
    y = 8
    for b in BSB:
        b["h"] = max(b["n"] * PX, MINH)
        b["y"] = y
        y += b["h"] + GAP
    H = y + 4
    ya = 8
    posB = {b["key"]: b for b in BSB}
    for b in BSA:
        b["h"] = max(b["n"] * PX, MINH)
        tgt = posB.get(b["key"])
        b["y"] = max(ya, tgt["y"]) if tgt else ya
        ya = b["y"] + b["h"] + GAP
    H = max(H, ya + 4)
    el = []
    order = ["identical", "tmn", "adapted", "new", "tm7only"]
    nm = {"identical": "identical", "tmn": "equal after normalizing the TM string", "adapted": "changed",
          "new": "ours only", "tm7only": "TM7 only"}

    def blk(b, x, side):
        g = []
        tot = b["n"] or 1
        xx = x
        for t in order:
            n = b["c"][t]
            if not n:
                continue
            w = BW * n / tot
            g.append(f'<rect class="f-{t}" x="{xx:.1f}" y="{b["y"]:.1f}" width="{w:.1f}" height="{b["h"]:.1f}"/>')
            xx += w
        g.append(f'<rect class="bo" x="{x}" y="{b["y"]:.1f}" width="{BW}" height="{b["h"]:.1f}" rx="2"/>')
        parts = ", ".join(f'{b["c"][t]} {nm[t]}' for t in order if b["c"][t])
        href = f'{TM7_HREF}#L-{b["l0"]}' if side == "a" else f'{esc(OURS_HREF)}#L-{b["l0"]}'
        tip = f'{"TM7" if side == "a" else "ours"} {b["label"]}: L{b["l0"]}–{b["l1"]}, {b["n"]} non-blank lines ({parts})'
        ty = b["y"] + min(b["h"], 30) / 2 + 5
        if side == "a":
            lab = f'<text class="bl" x="{x - 8}" y="{ty:.1f}" text-anchor="end">{E(b["label"])} <tspan class="bn">{b["n"]}</tspan></text>'
        else:
            lab = f'<text class="bl" x="{x + BW + 8}" y="{ty:.1f}">{E(b["label"])} <tspan class="bn">{b["n"]}</tspan></text>'
        return f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{href}" data-tip="{esc(tip)}"><title>{esc(tip)}</title>{"".join(g)}{lab}</a>'

    for b in BSA:
        tgt = posB.get(b["key"])
        if tgt:
            dashed = " role" if b["key"] == "dom" else ""
            el.append(f'<polygon class="sband{dashed}" points="{XA + BW},{b["y"]:.1f} {XA + BW},{b["y"] + b["h"]:.1f} '
                      f'{XB},{tgt["y"] + tgt["h"]:.1f} {XB},{tgt["y"]:.1f}"/>')
            if b["key"] == "dom":
                mx_ = (XA + BW + XB) / 2
                my_ = (b["y"] + tgt["y"]) / 2 + 22
                el.append(f'<text class="bl rl2" x="{mx_:.0f}" y="{my_:.0f}" text-anchor="middle">replaced by</text>')
    for b in BSA:
        el.append(blk(b, XA, "a"))
    for b in BSB:
        el.append(blk(b, XB, "b"))
    head = (f'<text class="hd" x="{XA + BW / 2}" y="-6" text-anchor="middle">TM7 ({nbA} non-blank lines)</text>'
            f'<text class="hd" x="{XB + BW / 2}" y="-6" text-anchor="middle">#2 ours ({nbB})</text>')
    return (f'<svg class="struct" viewBox="0 -24 1400 {H + 24:.0f}" role="img" aria-label="Proof structure: TM7 blocks vs ours, heights proportional to lines">'
            f'{head}{"".join(el)}</svg>')


_sl_b = [lab for _, lab, ns in BLOCKS_B if any(c[3] in ns for c in coincidental)]
_sl_a = [lab for _, lab, ns in BLOCKS_A if any(c[2] in ns for c in coincidental)]
SLIVER_TXT = (f" The thin grey slivers at the left of {' and '.join('“' + E(x) + '”' for x in _sl_b)} (ours) and of {' and '.join('“' + E(x) + '”' for x in _sl_a)} (TM7) "
              f"are the {len(coincidental)} coincidental <code>Proof.</code>/<code>Qed.</code> matches noted in section 2, not reused proof text."
              if coincidental else "")
CLAUSE_HTML = "".join(
    f'<tr><td><code>{E(c["name"])}</code></td><td>{tag_chip(c["clause"])}</td><td>{tag_chip(c["bullet"])}</td></tr>'
    for c in clause_rows)

S5 = f"""
{structure_svg()}
<p class="foot">Block height = non-blank lines (1 px each, at least 18 px so the label fits; the number after each label is the count). The fill inside a block splits its lines by diff status: grey identical, amber changed, green ours only, red TM7 only, blue the <code>tm</code> line (equal once the TM string is normalized). Grey bands join blocks with the same job; the dashed band is the replaced domain lemma. Each TM7 block is drawn level with its match. Click a block to open its first line.{SLIVER_TXT}</p>
<div class="s5">
<div class="s5l">
<h3>Why it grew: A1 at run time</h3>
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/img/eat_pair.png"><img src="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/img/eat_pair.png" alt="One eating pass: ours runs a +1 pass at each L, TM7 turns straight back" class="shot"></a>
<p class="foot">From <code>scripts/compare_tm7.py</code>: same start S(L⁴1L1). Each time ours fires A1 (0RF) it runs one extra pass (blue boxes) that adds +1 to the digits on its right; TM7's A1 (0RC) turns straight back.</p>
</div>
<div class="s5r">
<h3>What changed, and why</h3>
<ol class="why">
<li><b>New relation <code>Inc</code></b> for that +1 (on the 0/1 digits, little-endian binary, L skipped), and <code>Inc_spec</code>, which proves it is one <code>h</code> pass on the tape.</li>
<li><b>The two L clauses of <code>RIncs</code></b> (<code>RIncs_hx_ld</code>: the eater enters an L; <code>RIncs_h1_ld</code>: a drain pass enters an L) get an <code>Inc</code> premise and recurse on the incremented rest. Their <code>RIncs_spec</code> bullets now use <code>seg_hx_ld</code> / <code>seg_h1_ld</code>: the segment emits <code>h ++ h' ++ h^^(1+k)</code> instead of TM7's <code>h' ++ h^^(1+k)</code>.</li>
<li><b>Two zero-pass end clauses, Z1 and Z0</b> (<code>RIncs_h1_z1</code>, <code>RIncs_h1_z0</code>). They add no machine behaviour (<code>z1_eq</code>, <code>z0_eq</code> are tape identities). <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/proof.md.html">proof.md</a> §3.3: without them <code>LLLL10LL1L1</code> is in the domain but its sweep <code>LLLLL1LLLLLLL111</code> is not.</li>
<li><b>The domain lemma is redone.</b> TM7's <code>RIncs_nxt</code> (induction on r, automation <code>solve_v1/solve_v2</code>) becomes <code>key</code>: a second sweep reads the first one's output with <code>j</code> pending +1 passes, under the condition <code>Inv</code>, by induction on the derivation. At <code>j = 0</code>, <code>Inv</code> is TM7's condition. Helpers: <code>RIncs_Inc</code> (one more pass = +1 on the result), <code>End_1</code>/<code>End_x</code> (the right end, which TM7 handled inside <code>RIncs_nxt</code>), seven <code>inv_*</code> inversions, <code>Inc_total</code>/<code>Inc_fun</code>.</li>
<li><b>Reused verbatim:</b> the header tactics, the digit encoding and notations, <code>toRC</code>/<code>toH</code>, the segment tactics, <code>RIncs_nxt_1</code>, <code>lh</code>, <code>S'</code>, <code>BigStep</code>. <code>nonhalt</code> keeps its shape (<code>multistep_nonhalt</code> then <code>progress_nonhalt_cond</code>, same invariant) but starts from <code>S' [LD;D1]</code> (lemma <code>start</code>) instead of <code>S' [D1]</code>.</li>
</ol>
<h3>Clause by clause: <code>RIncs</code> and its <code>RIncs_spec</code> bullet</h3>
<table class="mx cl"><thead><tr><th>clause (ours, in order)</th><th>RIncs clause</th><th>RIncs_spec bullet</th></tr></thead><tbody>{CLAUSE_HTML}</tbody></table>
<p class="foot">RIncs: {cl_cnt['identical']} identical, {cl_cnt['adapted']} adapted, {cl_cnt['new']} new (TM7 has {len(clA)}). RIncs_spec bullets: {bu_cnt['identical']} identical, {bu_cnt['adapted']} adapted, {bu_cnt['new']} new. Bullet <i>n</i> proves clause <i>n</i> in both files.</p>
</div>
</div>"""

# ================================================================ section 6: submission comparison
n_single = len(single)
single_top = sum(1 for x in single if not x["module"])
single_end = sum(1 for x in single if x["ends_with_comment"])
single_fence = sum(1 for x in single if x["fence"])
fence_eg_x = next(x for x in single if x["fence"] and x["lines"] < 300)
fence_eg, fence_eg_rel = fence_eg_x["name"], fence_eg_x["rel"]
smin, smax = min(x["lines"] for x in single), max(x["lines"] for x in single)
cmin, cmax = min(x["comments"] for x in single), max(x["comments"] for x in single)
hdr_b0 = stats["ours_header_copy_at"]
c0 = ours_comments[0]
cl = ours_comments[-1]
nxt = A_by["RIncs_nxt"]
dupe_txt = "; ".join(
    f'{" = ".join("<code>" + bname(h) + "</code>" for h in v)} ({n + 1} lines each, only the case-label comment differs)'
    for v, n in key_dupes)
tail_txt = ", and ".join(
    f'{", ".join("<code>" + bname(h) + "</code>" for h in v)} end in the same {n} lines'
    for v, n, _ in key_tail_dupes) + (
    f" (they differ only in the label and their first {'line' if max(t[2] for t in key_tail_dupes) == 1 else 'one or two lines'}, "
    "the inversion step)")
hdr_cmt_html = code_lines(B, CLSB, c0["l0"], c0["l1"])
paths_html = ", ".join(f'{link_b(n)} <code>{E(p.rstrip("."))}</code>' for n, p in path_hits)
modlist = ", ".join(f"{m[0]}" for m in mods)
def _nb_neighbor(j, step):
    j += step
    while 0 <= j < len(bn) and not bn[j].strip():
        j += step
    return j if 0 <= j < len(bn) else None


added_blank_in_items = []
for op, i, j in ops:
    if op == "add" and not bn[j].strip():
        jp, jn = _nb_neighbor(j, -1), _nb_neighbor(j, 1)
        if jp is not None and jn is not None and opB[jp] in ("eq", "chg") and opB[jn] in ("eq", "chg"):
            added_blank_in_items.append(B[j][0])
new_names = [r["b"]["name"] for r in rows if r["tag"] == "new" and r["b"]["kind"] in KIND_GROUP]
inv_n = sum(1 for n in new_names if n.startswith("inv_"))
new_names_disp = []
for n in new_names:
    if n.startswith("inv_"):
        if "inv_*" not in new_names_disp:
            new_names_disp.append("inv_*")
    else:
        new_names_disp.append(n)
gone = [r["a"]["name"] for r in rows if r["tag"] == "tm7only"]

S6 = f"""
<div class="hscroll"><table class="cmp">
<thead><tr><th></th><th>TM7 upstream</th><th>#2 (our submission)</th></tr></thead>
<tbody>
<tr><th>Where it lives</th><td>One of {len(mods)} modules ({modlist}) in <code>SOMDCv6.v</code> ({len(somd)} lines), <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{SOMD_HREF}#L-{t7s + 1}">lines {t7s + 1}–{t7e + 1}</a>.</td>
<td>Its own file named by the machine string, {len(B)} lines, everything top level (no <code>Module</code>).</td></tr>
<tr><th>Shared header</th><td>{hdr_lines_n} lines at the top of the file (imports, <code>esc</code>, <code>ec</code>, <code>am</code>), used by all {len(mods)} modules.</td>
<td>The same {hdr_lines_n} lines copied verbatim at {link_b(hdr_b0, f"lines {hdr_b0}–{hdr_b0 + hdr_lines_n - 1}")}.</td></tr>
<tr><th>Comments</th><td>None: {somd_comments} comments in all {len(somd)} lines of SOMDCv6.v.</td>
<td>{len(ours_comments)} top-level comments ({ours_cmt_lines} lines) and {inline_cmt} inline ones (mostly the case labels in <code>key</code>).</td></tr>
<tr><th>Header comment</th><td><span class="muted">none</span></td>
<td>{link_b(c0["l0"], f"Lines {c0['l0']}–{c0['l1']}")}: machine, template and the A1 difference, mechanism in one line, informal-proof path, AI disclosure.</td></tr>
<tr><th>Rule table</th><td><span class="muted">none</span></td>
<td>{link_b(cl["l0"], f"Lines {cl['l0']}–{cl['l1']}")}: machine string, <code>S(r)</code>, the sweep rules, in a <code>```</code> block inside <code>(* *)</code>.</td></tr>
<tr><th>Names</th><td>Shared skeleton names, counted over the {len(mods)} modules: <code>RIncs_spec</code> ×{skel_counts['RIncs_spec']}, <code>RIncs_nxt</code> ×{skel_counts['RIncs_nxt']}, <code>nonhalt</code> ×{skel_counts['nonhalt']}, <code>BigStep</code> ×{skel_counts['BigStep']}, <code>RIncs_nxt_1</code> ×{skel_counts['RIncs_nxt_1']}.</td>
<td>Keeps every TM7 name except {", ".join(f"<code>{E(n)}</code>" for n in gone)}. {len(new_names)} new names: {", ".join(f"<code>{E(n)}</code>" + (f" ({inv_n})" if n == "inv_*" else "") for n in new_names_disp)}.</td></tr>
<tr><th>Domain lemma</th><td><code>RIncs_nxt</code>, {nxt['l1'] - nxt['l0'] + 1} lines; the cases are closed by two Ltacs (<code>solve_v1</code>, <code>solve_v2</code>).</td>
<td><code>key</code>, {key_len} lines ({pct(key_len, len(B))} of the file); every case written out.</td></tr>
<tr><th>Final theorem</th><td><code>Lemma nonhalt: ~halts tm c0.</code> inside <code>Module TM7</code>.</td><td>The same statement at top level ({link_b(next(x['l0'] for x in IB if x['name'] == 'nonhalt'))}), as <code>tools/check_kill.sh</code> requires.</td></tr>
</tbody></table></div>
<p class="foot">Upstream also has single-machine files: {n_single} <code>.v</code> files under <code>verify/</code> are named by their machine string ({smin}–{smax} lines). {single_top} of them are top level and {n_single - single_top} wrap{"s" if n_single - single_top == 1 else ""} its proof in a <code>Module</code>. They have {cmin}–{cmax} comments each, {single_end} end with a comment, and {single_fence} put rules in a <code>```</code> block inside it (e.g. <a href="/busy-beaver/machines/vendor/busycoq/verify/</span><span class="si">{esc(fence_eg_rel)}">{E(fence_eg)}</a>). Our layout (top-level <code>tm</code>, trailing rule comment) follows that convention. The header comment has no upstream counterpart.</p>

<h3>Our header comment</h3>
<pre class="code">{hdr_cmt_html}</pre>

<h3>What a maintainer might raise</h3>
<ol class="notes">
{f"<li><b>Repo-local paths in the header comment.</b> {paths_html}. These paths exist in our repo; in busycoq the template is <code>verify/SOMDCv6.v</code>, and the other two files are not there.</li>" if path_hits else
   "<li><b>No repo-local paths in the header comment.</b> It names the template as <code>verify/SOMDCv6.v</code> (busycoq's own layout), the informal proof as the accompanying write-up (proof.md), and the check by busycoq commit, Coq version and the <code>Print Assumptions</code> result. Until the comment-only edit of 2026-10-10 it named <code>vendor/busycoq/verify/SOMDCv6.v</code>, <code>machines/…/proof.md</code> and <code>tools/check_kill.sh</code>.</li>"}
<li><b>Repeated case text in <code>key</code>.</b> Byte-identical bullets: {dupe_txt}. Also {tail_txt}. TM7 folds its repeated cases into <code>solve_v1</code>/<code>solve_v2</code>; a local Ltac could do the same here.</li>
<li><b>Length.</b> {len(B)} lines against TM7's {N['tm7_module']}-line module ({len(A)} with the shared header). <code>key</code> alone is {key_len} lines. The {D['added']} added non-blank lines are marked in <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#s4">section 4</a>; <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#s3">section 3</a> lists the {tag_tot['new']} new items they make up.</li>
<li><b>AI disclosure inside the file</b> ({link_b(c0['l1'])}). Upstream proofs carry no authorship or AI line: of the {len(all_v)} <code>.v</code> files under <code>verify/</code> ({len(all_v_top)} at the top, the rest in subfolders), a search for author / written by / Claude / GPT / LLM / AI-assisted matches only {", ".join(f"<code>{E(x)}</code>" for x in auth_hits)}{" (a third-party library's license note)" if auth_hits == ["LibTactics.v"] else ""}. The same disclosure is in <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/submission/README.md.html">submission/README.md</a> and <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/submission/discord.md.html">discord.md</a>, so it could live only there if a maintainer prefers.</li>
<li><b>Generic names.</b> <code>key</code>, <code>Inv</code>, <code>domain</code>, <code>start</code> are fine in a single file but say less than the template's style. proof.md calls <code>key</code> <code>RIncs_nxt'</code>.</li>
<li><b>Cosmetic drift from TM7</b>, which makes the diff a little noisier: {ws_only} whitespace-only change (<code>apply BigStep,I1</code> → <code>apply BigStep, I1</code>), {len(added_blank_in_items)} blank line{"s" if len(added_blank_in_items) != 1 else ""} added between two lines kept from TM7 ({", ".join(f"<code>{E(owner(IB, n - 1))}</code> " + link_b(n) for n in added_blank_in_items)}), and a final <code>Close Scope sym.</code> that TM7 does not have.</li>
</ol>"""

# ================================================================ page
CSS = r"""
:root{color-scheme:light;
 --page:#f7f7f5;--surface:#ffffff;--sunk:#f0efec;--ink:#151514;--ink2:#4b4a46;--muted:#75736d;
 --line:#e3e1db;--axis:#c3c2b7;--accent:#2457c5;--accent-weak:rgba(36,87,197,.10);--code:#f3f2ee;
 --t-identical:#b4b2a9;--t-adapted:#eda100;--t-new:#1baf7a;--t-tm7only:#e34948;--t-tmn:#8e9ad6;
 --bg-adapted:rgba(237,161,0,.14);--bg-new:rgba(27,175,122,.11);--bg-tm7only:rgba(227,73,72,.10);--bg-tmn:rgba(36,87,197,.08);
 --mk-d:rgba(227,73,72,.30);--mk-i:rgba(27,175,122,.30);--band:rgba(120,118,110,.20);--band-ad:rgba(237,161,0,.35);
 --sx-kv:#7a3e9d;--sx-kt:#1f5fa8;--sx-cm:#5f7a63;--sx-st:#a3401b;--sx-nu:#8a5a00;--sx-op:#8a877f;--sx-nb:#a3401b}
@media (prefers-color-scheme:dark){:root:not([data-theme="light"]){color-scheme:dark;
 --page:#111110;--surface:#1a1a19;--sunk:#232321;--ink:#f2f1ed;--ink2:#c8c6bf;--muted:#98968e;
 --line:#2f2f2c;--axis:#4a4a44;--accent:#82a8f0;--accent-weak:rgba(130,168,240,.15);--code:#1d1d1b;
 --t-identical:#5f5e58;--t-adapted:#c98500;--t-new:#199e70;--t-tm7only:#e66767;--t-tmn:#7d8fd8;
 --bg-adapted:rgba(201,133,0,.17);--bg-new:rgba(25,158,112,.15);--bg-tm7only:rgba(230,103,103,.13);--bg-tmn:rgba(130,168,240,.10);
 --mk-d:rgba(240,110,110,.36);--mk-i:rgba(60,200,140,.33);--band:rgba(200,198,190,.14);--band-ad:rgba(201,133,0,.40);
 --sx-kv:#c79bf2;--sx-kt:#7fb0f0;--sx-cm:#8fa592;--sx-st:#e8a07a;--sx-nu:#e0b45a;--sx-op:#8f8c84;--sx-nb:#e8a07a}}
:root[data-theme="dark"]{color-scheme:dark;
 --page:#111110;--surface:#1a1a19;--sunk:#232321;--ink:#f2f1ed;--ink2:#c8c6bf;--muted:#98968e;
 --line:#2f2f2c;--axis:#4a4a44;--accent:#82a8f0;--accent-weak:rgba(130,168,240,.15);--code:#1d1d1b;
 --t-identical:#5f5e58;--t-adapted:#c98500;--t-new:#199e70;--t-tm7only:#e66767;--t-tmn:#7d8fd8;
 --bg-adapted:rgba(201,133,0,.17);--bg-new:rgba(25,158,112,.15);--bg-tm7only:rgba(230,103,103,.13);--bg-tmn:rgba(130,168,240,.10);
 --mk-d:rgba(240,110,110,.36);--mk-i:rgba(60,200,140,.33);--band:rgba(200,198,190,.14);--band-ad:rgba(201,133,0,.40);
 --sx-kv:#c79bf2;--sx-kt:#7fb0f0;--sx-cm:#8fa592;--sx-st:#e8a07a;--sx-nu:#e0b45a;--sx-op:#8f8c84;--sx-nb:#e8a07a}
*{box-sizing:border-box}
html{background:var(--page)}
body{margin:0;background:var(--page);color:var(--ink);font:15px/1.5 system-ui,-apple-system,"Segoe UI",sans-serif}
a{color:var(--accent);text-decoration:none}a:hover{text-decoration:underline}
code,pre,.mono{font-family:ui-monospace,"Cascadia Code",Consolas,Menlo,monospace}
code{font-size:.88em;background:var(--code);padding:0 .25em;border-radius:3px}
.muted{color:var(--muted)}.small{font-size:13px}
.wrap{max-width:1480px;margin:0 auto;padding:14px 24px 60px}
header.top{display:flex;flex-wrap:wrap;align-items:baseline;gap:4px 14px;padding-bottom:10px;border-bottom:1px solid var(--line)}
header.top .rank{font-weight:700;font-size:17px;color:var(--muted)}
header.top h1{font-size:19px;margin:0;font-weight:650}
header.top .links{display:flex;flex-wrap:wrap;gap:2px 14px;font-size:13.5px;margin-left:auto}
.lede{margin:12px 0 4px;font-size:15.5px;color:var(--ink2);max-width:1100px}
.lede b{color:var(--ink)}
nav.toc{display:flex;flex-wrap:wrap;gap:6px;margin:12px 0 4px}
nav.toc a{border:1px solid var(--line);background:var(--surface);border-radius:999px;padding:2px 11px;font-size:13px;color:var(--ink2)}
nav.toc a b{color:var(--muted);margin-right:4px}
section{margin-top:30px;padding-top:6px}
section>h2{display:flex;align-items:baseline;gap:10px;font-size:20px;margin:0 0 4px;font-weight:650}
section>h2 .num{display:inline-flex;align-items:center;justify-content:center;width:26px;height:26px;border-radius:50%;
 background:var(--ink);color:var(--page);font-size:14px;font-weight:700;flex:none;transform:translateY(-2px)}
.notice{margin:0 0 14px;padding:6px 12px;border-left:4px solid var(--accent);background:var(--accent-weak);border-radius:0 6px 6px 0;font-size:14.5px}
.notice b{font-weight:650}
h3{font-size:14px;margin:18px 0 8px;font-weight:650}
h3 .muted{font-weight:400}
.foot{font-size:12.5px;color:var(--muted);margin:8px 0 0;max-width:1150px}
.foot code{font-size:.92em}
ul.tight{margin:4px 0 8px;padding-left:18px}ul.tight li{margin:2px 0}
.btn{display:inline-block;border:1px solid var(--accent);border-radius:6px;padding:3px 12px;font-weight:600;font-size:14px;margin-right:8px}
/* tags */
.tag{display:inline-flex;align-items:center;gap:5px;font-size:12px;font-weight:600;white-space:nowrap;color:var(--ink)}
.tag i{width:10px;height:10px;border-radius:2px;display:inline-block;background:var(--t-identical)}
.tag.t-adapted i{background:var(--t-adapted)}.tag.t-new i{background:var(--t-new)}.tag.t-tm7only i{background:var(--t-tm7only)}
/* section 1 */
.tmrow{display:flex;flex-wrap:wrap;gap:18px;align-items:flex-start}
figure.tmt{margin:0;background:var(--surface);border:1px solid var(--line);border-radius:8px;padding:10px 12px}
figure.tmt.ours{border-color:var(--accent)}
figure.tmt figcaption{display:flex;flex-direction:column;margin-bottom:6px;font-size:14px}
figure.tmt figcaption span{font-size:12px;color:var(--muted)}
table.tt{border-collapse:collapse;font:14px/1.3 ui-monospace,"Cascadia Code",Consolas,monospace}
table.tt th,table.tt td{padding:4px 10px;border:1px solid var(--line);text-align:center}
table.tt thead th{font:600 11.5px system-ui,sans-serif;color:var(--muted);border-top:0}
table.tt tbody th{font-weight:700;color:var(--ink2);border-left:0}
table.tt td.a1{outline:2px solid var(--accent);outline-offset:-2px;font-weight:700}
table.tt td.neq{background:var(--bg-adapted);font-weight:700}
.tmside{flex:1 1 380px;min-width:300px;font-size:14px}
.tmside p{margin:4px 0}
.tmside .k{font-size:12px;font-weight:650;letter-spacing:.06em;text-transform:uppercase;color:var(--muted);margin-top:12px}
.tmside code mark{background:var(--bg-adapted);color:inherit;font-weight:700;outline:1.5px solid var(--t-adapted);border-radius:2px}
/* section 2 */
.tiles{display:flex;flex-wrap:wrap;gap:12px}
.tile{background:var(--surface);border:1px solid var(--line);border-radius:8px;padding:10px 14px;min-width:170px;flex:1 1 170px}
.tile.hl{border-color:var(--accent)}
.tile .big{font-size:28px;font-weight:700;font-variant-numeric:tabular-nums;line-height:1.1}
.tile .big small{font-size:16px;color:var(--muted);font-weight:600}
.tile .lab{font-size:13px;color:var(--ink2);margin-top:3px}
.barrow{display:grid;grid-template-columns:190px 1fr;gap:12px;align-items:start;margin:8px 0 12px}
.barlab{display:flex;flex-direction:column;font-size:14px}.barlab span{font-size:12px;color:var(--muted)}
.bar{display:flex;gap:2px;height:30px}
.seg{border-radius:3px;display:flex;align-items:center;padding:0 8px;overflow:hidden;min-width:3px}
.seg span{font-size:12.5px;font-weight:650;white-space:nowrap;color:#151514}
.s-identical{background:var(--t-identical)}.s-adapted{background:var(--t-adapted)}.s-new{background:var(--t-new)}.s-tm7only{background:var(--t-tm7only)}.s-tmn{background:var(--t-tmn)}
@media (prefers-color-scheme:dark){:root:not([data-theme="light"]) .s-identical span{color:#f2f1ed}}
:root[data-theme="dark"] .s-identical span{color:#f2f1ed}
.barleg{display:flex;flex-wrap:wrap;gap:4px 16px;margin-top:5px;font-size:13px;color:var(--ink2)}
.lg{display:inline-flex;align-items:center;gap:6px;font-size:13px;color:var(--ink2);white-space:nowrap}
.lg i{width:11px;height:11px;border-radius:2px;display:inline-block}
.lg b{color:var(--ink);font-variant-numeric:tabular-nums}
svg.ribbon{width:100%;height:auto;display:block;margin-top:4px;max-width:1300px}
svg .band{fill:var(--band)}svg .band.b-adapted{fill:var(--band-ad)}svg .band.b-tmn{fill:var(--t-tmn);opacity:.55}svg .f-tmn{fill:var(--t-tmn)}
svg .f-identical{fill:var(--t-identical)}svg .f-adapted{fill:var(--t-adapted)}svg .f-new{fill:var(--t-new)}svg .f-tm7only{fill:var(--t-tm7only)}
svg a:hover .band{fill:var(--accent-weak);stroke:var(--accent);stroke-width:.8}
svg a:hover rect{stroke:var(--ink);stroke-width:.8}
svg text.rl{font:12px system-ui,sans-serif;fill:var(--muted)}
.readout{font-size:13px;color:var(--ink2);min-height:20px;margin:2px 0 0;font-variant-numeric:tabular-nums}
.two{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1fr);gap:28px}
table.mx{border-collapse:collapse;font-size:13.5px;background:var(--surface);border:1px solid var(--line);border-radius:6px}
table.mx th,table.mx td{padding:4px 10px;border-bottom:1px solid var(--line);text-align:right;font-variant-numeric:tabular-nums}
table.mx thead th{font-size:12px;color:var(--muted);font-weight:600}
table.mx tbody th{text-align:left;font-weight:500}
table.mx tr.tot th,table.mx tr.tot td{color:var(--muted);border-bottom:0}
table.mx.cl td,table.mx.cl th{text-align:left}
/* section 3 */
.ctl{display:flex;flex-wrap:wrap;gap:6px;align-items:center;margin:4px 0 10px}
.ctl .sp{flex:1}
button{font:13px system-ui,sans-serif;border:1px solid var(--line);background:var(--surface);color:var(--ink2);border-radius:6px;padding:3px 10px;cursor:pointer}
button:hover{border-color:var(--accent);color:var(--ink)}
button.flt.on{background:var(--ink);color:var(--page);border-color:var(--ink)}
button.flt b{font-variant-numeric:tabular-nums;margin-left:3px}
.ithead,.it>summary{display:grid;grid-template-columns:96px 84px minmax(0,1.15fr) minmax(0,1.15fr) minmax(0,1.6fr);gap:10px;align-items:baseline}
.ithead{font-size:12px;font-weight:650;color:var(--muted);padding:0 12px 4px 30px;border-bottom:1px solid var(--line)}
.items{border:1px solid var(--line);border-radius:8px;background:var(--surface);overflow:hidden}
.it{border-bottom:1px solid var(--line)}
.it:last-child{border-bottom:0}
.it>summary{list-style:none;cursor:pointer;padding:5px 12px 5px 12px;font-size:13.5px;position:relative;padding-left:30px}
.it>summary::-webkit-details-marker{display:none}
.it>summary::before{content:"▸";position:absolute;left:12px;top:5px;color:var(--muted);font-size:12px}
.it[open]>summary::before{content:"▾"}
.it>summary:hover{background:var(--sunk)}
.it.role{background:var(--accent-weak)}
.it.t-adapted>summary{box-shadow:inset 3px 0 0 var(--t-adapted)}
.it.t-new>summary{box-shadow:inset 3px 0 0 var(--t-new)}
.it.t-tm7only>summary{box-shadow:inset 3px 0 0 var(--t-tm7only)}
.c-kind{font-size:12px;color:var(--muted)}
.c-a,.c-b{min-width:0;overflow-wrap:anywhere}
.c-a code,.c-b code{font-size:12.5px;background:none;padding:0;font-weight:600;color:var(--ink)}
.c-a .muted,.c-b .muted{font-size:12px}
a.ln{font:12px ui-monospace,Consolas,monospace;margin-left:4px}
.c-note{font-size:12.5px;color:var(--ink2)}
.cmt{font:12px ui-monospace,Consolas,monospace;color:var(--sx-cm)}
.ib{padding:4px 14px 12px 30px;background:var(--sunk);border-top:1px dashed var(--line)}
.ib .bh{font-size:12.5px;color:var(--ink2);margin:6px 0}
pre.code{margin:0;background:var(--code);border:1px solid var(--line);border-radius:6px;padding:8px 10px;font-size:12.5px;line-height:1.45;
 white-space:pre-wrap;overflow-wrap:anywhere;max-height:520px;overflow:auto}
pre.code .lno{display:inline-block;width:4.6em;white-space:nowrap;color:var(--muted);user-select:none;text-align:right;padding-right:12px}
.pair{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1fr);gap:10px}
/* syntax */
.kv{color:var(--sx-kv);font-weight:600}.kt{color:var(--sx-kt)}.cm{color:var(--sx-cm);font-style:italic}.st{color:var(--sx-st)}
.nu{color:var(--sx-nu)}.op{color:var(--sx-op)}.nb{color:var(--sx-nb)}
.xd{background:var(--mk-d);text-decoration:line-through;text-decoration-thickness:1px;border-radius:2px}
.xi{background:var(--mk-i);border-radius:2px;text-decoration:none}
del.xd,ins.xi{padding:0 2px}
/* section 4 */
.ctl.sticky{position:sticky;top:0;z-index:5;background:var(--page);padding:6px 0;border-bottom:1px solid var(--line)}
.sbswrap{border:1px solid var(--line);border-radius:8px;overflow:hidden;background:var(--surface)}
table.sbs{width:100%;border-collapse:collapse;table-layout:fixed;font:12.5px/1.42 ui-monospace,"Cascadia Code",Consolas,monospace}
table.sbs col.cl{width:46px}table.sbs col.cm{width:18px}
table.sbs thead th{font:600 12.5px system-ui,sans-serif;text-align:left;padding:6px 10px;background:var(--sunk);border-bottom:1px solid var(--line)}
table.sbs td{padding:0 6px;vertical-align:top}
table.sbs td.ln{text-align:right;color:var(--muted);user-select:none;padding-right:8px;border-right:1px solid var(--line)}
table.sbs td.ln a{color:var(--muted)}
table.sbs td.cd{white-space:pre-wrap;overflow-wrap:anywhere}
table.sbs td.mk{text-align:center;color:var(--muted);font-weight:700;border-right:1px solid var(--line)}
table.sbs td.cd.empty{background:repeating-linear-gradient(135deg,transparent 0 5px,var(--sunk) 5px 7px)}
tr.chg td.cd{background:var(--bg-adapted)}tr.chg td.mk{color:var(--t-adapted)}
tr.del td.cd:not(.empty){background:var(--bg-tm7only)}tr.del td.mk{color:var(--t-tm7only)}
tr.add td.cd:not(.empty){background:var(--bg-new)}tr.add td.mk{color:var(--t-new)}
tr.tmn td.cd{background:var(--bg-tmn)}tr.tmn td.mk{color:var(--t-tmn)}
tr.tmn .xd,tr.tmn .xi{text-decoration:none;background:var(--bg-adapted);outline:1.5px solid var(--t-adapted)}
tr:target td,tr.flash td{box-shadow:inset 0 2px 0 var(--accent)}
tbody.foldbar td{padding:0;background:var(--sunk);border-top:1px solid var(--line);border-bottom:1px solid var(--line)}
button.fold{width:100%;text-align:left;border:0;border-radius:0;background:none;padding:3px 12px;font:12.5px system-ui,sans-serif;color:var(--ink2)}
button.fold:hover{background:var(--accent-weak)}
.fx{display:inline-block;width:12px}
/* section 5 */
.s5{display:grid;grid-template-columns:minmax(0,560px) minmax(0,1fr);gap:28px;align-items:start;margin-top:14px}
svg.struct{width:100%;height:auto;display:block}
svg.struct .bo{fill:none;stroke:var(--axis);stroke-width:1}
svg.struct a:hover .bo{stroke:var(--ink);stroke-width:1.6}
svg.struct .sband{fill:var(--band)}
svg.struct .sband.role{fill:none;stroke:var(--t-tm7only);stroke-dasharray:4 3;stroke-width:1.2}
svg.struct text.bl{font:13.5px system-ui,sans-serif;fill:var(--ink2)}
svg.struct text.rl2{fill:var(--t-tm7only);font-style:italic}
svg.struct .bn{fill:var(--muted);font-variant-numeric:tabular-nums}
svg.struct text.hd{font:600 14.5px system-ui,sans-serif;fill:var(--ink)}
svg.struct{max-width:1400px}
img.shot{width:100%;max-width:560px;border-radius:6px;border:1px solid var(--line);display:block}
ol.why{padding-left:20px;margin:10px 0}ol.why li{margin:6px 0;font-size:14px}
/* section 6 */
table.cmp{border-collapse:collapse;width:100%;background:var(--surface);border:1px solid var(--line);border-radius:8px;font-size:14px}
table.cmp th,table.cmp td{text-align:left;vertical-align:top;padding:7px 12px;border-bottom:1px solid var(--line)}
table.cmp thead th{font-size:12.5px;color:var(--muted);font-weight:650;background:var(--sunk)}
table.cmp tbody th{width:150px;font-weight:600;color:var(--ink2)}
table.cmp td{width:43%}
ol.notes{padding-left:20px}ol.notes li{margin:7px 0;font-size:14px;max-width:1150px}
.hscroll{overflow-x:auto;max-width:100%}
.foot a,.foot code,ol.notes a,ol.notes code,.lede code{overflow-wrap:anywhere}
footer{margin-top:40px;padding-top:10px;border-top:1px solid var(--line);font-size:12px;color:var(--muted)}
@media (max-width:1100px){.s5,.two{grid-template-columns:minmax(0,1fr)}}
@media (max-width:760px){.wrap{padding:12px 16px 40px}
 .ithead{display:none}.it>summary{grid-template-columns:1fr 1fr;row-gap:2px}.c-note{grid-column:1/-1}
 .barrow{grid-template-columns:1fr}.pair{grid-template-columns:1fr}
 table.sbs{font-size:11px}table.sbs col.cl{width:34px}}
"""

JS = r"""
(function(){
  const $=(s,r=document)=>Array.from(r.querySelectorAll(s));
  // section 3 filters
  $('.flt').forEach(b=>b.addEventListener('click',()=>{
    $('.flt').forEach(x=>x.classList.toggle('on',x===b));
    const f=b.dataset.f;
    $('.items .it').forEach(d=>{d.hidden=!(f==='all'||d.dataset.tag===f);});
  }));
  function act(a){
    if(a==='open-adapted'){$('.items .it[data-tag="adapted"]').forEach(d=>d.open=true);}
    if(a==='close-all'){$('.items .it').forEach(d=>d.open=false);}
    if(a==='expand'){$('tbody.fold').forEach(t=>setFold(t,true));}
    if(a==='collapse'){$('tbody.fold').forEach(t=>setFold(t,false));}
    if(a==='next'||a==='prev'){
      const rows=$('tr[data-chg]');const top=document.querySelector('.ctl.sticky').getBoundingClientRect().bottom+4;
      let t=null;
      if(a==='next'){t=rows.find(r=>r.getBoundingClientRect().top>top+2);}
      else{const before=rows.filter(r=>r.getBoundingClientRect().top<top-2);t=before[before.length-1];}
      if(t){flash(t);}
    }
  }
  $('button.act').forEach(b=>b.addEventListener('click',()=>act(b.dataset.act)));
  function setFold(tb,open){
    tb.hidden=!open;const bar=tb.previousElementSibling;
    if(bar){const b=bar.querySelector('button.fold');b.setAttribute('aria-expanded',open);b.querySelector('.fx').textContent=open?'▾':'▸';}
  }
  $('button.fold').forEach(b=>b.addEventListener('click',()=>{
    const tb=b.closest('tbody').nextElementSibling;setFold(tb,tb.hidden);
  }));
  function flash(tr){
    const tb=tr.closest('tbody');if(tb&&tb.hidden)setFold(tb,true);
    const off=document.querySelector('.ctl.sticky').offsetHeight+8;
    window.scrollTo({top:tr.getBoundingClientRect().top+window.scrollY-off,behavior:'smooth'});
    $('tr.flash').forEach(x=>x.classList.remove('flash'));tr.classList.add('flash');
  }
  // ribbon / structure hover readout, and in-page jumps
  const ro=document.getElementById('ribbon-readout');const ro0=ro?ro.textContent:'';
  $('svg.ribbon [data-tip]').forEach(a=>{
    a.addEventListener('mouseenter',()=>{ro.textContent=a.dataset.tip;});
    a.addEventListener('mouseleave',()=>{ro.textContent=ro0;});
    a.addEventListener('click',e=>{const id=a.getAttribute('href').slice(1);const tr=document.getElementById(id);
      if(tr){e.preventDefault();history.replaceState(null,'','#'+id);flash(tr);}});
  });
  $('a.jump').forEach(a=>a.addEventListener('click',e=>{const id=a.getAttribute('href').slice(1);const tr=document.getElementById(id);
    if(tr){e.preventDefault();history.replaceState(null,'','#'+id);flash(tr);}}));
})();
"""

TITLE = "#2 vs TM7 compare"
NAV = "".join(f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#s</span><span class="si">{n}"><b>{n}</b>{t}</a>' for n, t in [
    (1, "The machines"), (2, "Similarity at a glance"), (3, "Item by item"), (4, "Full side-by-side diff"),
    (5, "Proof structure"), (6, "Submission")])


def section(n, title, notice, body):
    return (f'<section id="s{n}"><h2><span class="num">{n}</span>{title}</h2>'
            f'<p class="notice"><b>What to notice:</b> {notice}</p>{body}</section>')


notice1 = (f"one cell of 12 differs: A1 is <code>{C_7[('A', 1)]}</code> in TM7 and <code>{C_OURS[('A', 1)]}</code> in #2. "
           f"TM8 differs in the same cell (<code>{C_8[('A', 1)]}</code>) and uses TM7's proof text.")
notice2 = (f"{kept} of TM7's {nbA} non-blank lines ({pct(kept, nbA)}) appear unchanged in ours. Ours is "
           f"{N['ours'] / N['tm7_plus_header']:.1f}&times; longer, almost all of it added lines ({D['added']}), not edits ({D['changed']}).")
notice3 = (f"{tag_tot['identical']} items are identical and only {tag_tot['adapted']} are adapted (<code>tm</code>, "
           f"<code>RIncs</code>, <code>RIncs_spec</code>, <code>nonhalt</code>). The bulk is {tag_tot['new']} new items. "
           f"Open a row for its word diff or code.")
notice4 = ("long folded grey runs are TM7 kept verbatim. The colored stretches are where ours departs: the two "
           "<code>RIncs</code> L clauses, two <code>RIncs_spec</code> bullets, the new lemmas, and <code>nonhalt</code>.")
notice5 = ("the machine-facing half (encoding, tactics, <code>RIncs_spec</code>, <code>BigStep</code>) is reused; "
           "the domain argument is what grew, because A1's extra +1 pass breaks TM7's domain lemma.")
notice6 = ("ours follows upstream's single-machine-file layout (top-level <code>tm</code>, trailing rule comment), "
           "but adds a header comment" + (" with repo-local paths" if path_hits else "") +
           " and a much longer, unfactored domain lemma.")

PAGE = f"""<!doctype html>
<html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width, initial-scale=1">
<title>{E(TITLE)}</title><link rel="icon" href="data:,"><style>{CSS}</style></head><body><div class="wrap">
<header class="top"><span class="rank">#2</span><h1>Our proof vs its template, SOMDCv6.v Module TM7</h1>
<nav class="links"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/index.html#mechanism">machine page</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/review.html">review</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{esc(OURS_HREF)}">our .v</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/proof.md.html">proof.md</a>
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/submission/README.md.html">submission</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{TM7_HREF}">TM7 (highlighted)</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/</span><span class="si">{SOMD_HREF}#L-{t7s + 1}">SOMDCv6.v</a>
<a href="/busy-beaver/machines/tools/explorer/index.html#preset=p2-vs-tm7">explorer</a></nav></header>
<p class="lede"><code>{E(TM)}</code> was proved by extending mxdys's <b>TM7</b> from <code>vendor/busycoq/verify/SOMDCv6.v</code>, a machine that differs in one transition.
This page measures how much of TM7's proof text we kept, and shows every difference.</p>
<nav class="toc">{NAV}</nav>
{section(1, "The machines", notice1, S1)}
{section(2, "Similarity at a glance", notice2, S2)}
{section(3, "Item by item", notice3, S3)}
{section(4, "Full side-by-side diff", notice4, S4)}
{section(5, "Proof structure", notice5, S5)}
{section(6, "Submission comparison", notice6, S6)}
<footer>Generated by <code>compare/build.py</code> from <code>{E(stats['files']['ours'])}</code> (sha256 {stats['files']['ours_sha256'][:12]}…) and
<code>{E(stats['files']['somd'])}</code> (sha256 {stats['files']['somd_sha256'][:12]}…). Numbers: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/compare/stats.json">compare/stats.json</a>.</footer>
</div><script>{JS}</script></body></html>
"""
OUT.write_text(PAGE, encoding="utf-8")

# ================================================================ compare/TM7.html
st_of = {}
for op, i, j in ops:
    if i is not None:
        st_of[A[i][0]] = (op, B[j][0] if j is not None else None)
TROWS = []
STLAB = {"eq": ("identical", "kept verbatim in ours"), "chg": ("adapted", "changed in ours"),
         "del": ("tm7only", "not in ours")}
prev = None
for n, t in tm7_show:
    if prev is not None and n != prev + 1:
        TROWS.append(f'<tr class="gap"><td colspan="4">lines {prev + 1}–{n - 1}: Modules {", ".join(m[0] for m in mods if m[1] + 1 > prev and m[2] + 1 < n)} '
                     f'(not shown; <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/</span><span class="si">{SOMD_HREF}#L-{prev + 1}">full file</a>)</td></tr>')
    prev = n
    if n in st_of:
        op, bn_ = st_of[n]
        if op == "eq" and A[[x for x, _ in A].index(n)][1] != (B[bn_ - 1][1] if bn_ else None):
            cls, lab = "tmn", "equal after normalizing the TM string (A1 differs)"
        else:
            cls, lab = STLAB[op]
        to = f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/</span><span class="si">{esc(OURS_HREF)}#L-{bn_}">ours L{bn_}</a>' if bn_ else ""
    else:
        cls, lab, to = "wrap", "module wrapper (left out of the diff)", ""
    if not t.strip():
        cls_show = "blank"
    else:
        cls_show = cls
    TROWS.append(f'<tr id="L-{n}" class="g-{cls_show}" title="{esc(lab)}"><td class="g"></td><td class="ln"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare/build.py.html#L-</span><span class="si">{n}">{n}</a></td>'
                 f'<td class="cd">{render(t, CLS7[n])}</td><td class="to">{to if t.strip() else ""}</td></tr>')
TM7_PAGE = f"""<!doctype html>
<html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width, initial-scale=1">
<title>TM7 template copy</title><link rel="icon" href="data:,"><style>{CSS}
table.src{{border-collapse:collapse;width:100%;font:12.5px/1.45 ui-monospace,"Cascadia Code",Consolas,monospace;background:var(--surface);border:1px solid var(--line)}}
table.src td{{padding:0 8px;vertical-align:top}}
table.src td.g{{width:6px;padding:0}}
table.src td.ln{{width:52px;text-align:right;color:var(--muted);border-right:1px solid var(--line);user-select:none}}
table.src td.ln a{{color:var(--muted)}}
table.src td.cd{{white-space:pre-wrap;overflow-wrap:anywhere}}
table.src td.to{{width:90px;font-size:11.5px;text-align:right}}
tr.g-identical td.g{{background:var(--t-identical)}}tr.g-adapted td.g{{background:var(--t-adapted)}}
tr.g-tm7only td.g{{background:var(--t-tm7only)}}tr.g-tm7only td.cd{{background:var(--bg-tm7only)}}
tr.g-adapted td.cd{{background:var(--bg-adapted)}}tr.g-tmn td.g{{background:var(--t-tmn)}}tr.g-tmn td.cd{{background:var(--bg-tmn)}}
tr.g-wrap td.cd{{color:var(--muted)}}
tr.gap td{{background:var(--sunk);color:var(--muted);font:12.5px system-ui,sans-serif;padding:5px 12px;border-top:1px solid var(--line);border-bottom:1px solid var(--line)}}
tr:target td{{background:var(--accent-weak)!important}}
</style></head><body><div class="wrap">
<header class="top"><h1>SOMDCv6.v: shared header + Module TM7</h1>
<nav class="links"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/compare.html">&larr; compare page</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/</span><span class="si">{SOMD_HREF}#L-{t7s + 1}">full SOMDCv6.v</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/</span><span class="si">{esc(OURS_HREF)}">our .v</a></nav></header>
<p class="lede">Verbatim copy of <code>vendor/busycoq/verify/SOMDCv6.v</code> (busycoq 0940bb9c, sha256 <code>{stats['files']['somd_sha256'][:16]}…</code>), lines 1–{hdr_lines_n} and {t7s + 1}–{t7e + 1}.
Line numbers and anchors (<code>#L-&lt;n&gt;</code>) are SOMDCv6.v's own. The left stripe says what happened to each line in our proof.</p>
<p class="small"><span class="lg"><i class="s-identical"></i>kept verbatim</span> &nbsp; <span class="lg"><i class="s-adapted"></i>changed</span> &nbsp;
<span class="lg"><i class="s-tm7only"></i>not in ours</span> &nbsp; <span class="lg"><i class="s-tmn"></i>equal after normalizing the TM string</span> &nbsp;
<span class="muted">The right column links to the matching line in ours.</span></p>
<table class="src"><tbody>{"".join(TROWS)}</tbody></table>
<p class="foot">Lines {t7e + 2}–{len(somd)}: Module TM8, whose body equals TM7's except the <code>tm</code> line (A1 = <code>{C_8[('A', 1)]}</code>).</p>
</div></body></html>
"""
OUT_TM7.write_text(TM7_PAGE, encoding="utf-8")
print(f"wrote {OUT} ({len(PAGE) // 1024} KB), {OUT_TM7} ({len(TM7_PAGE) // 1024} KB), {OUT_STATS}")
print(json.dumps({"diff_nonblank": D, "tags": dict(tag_tot), "toplevel_faithful": TOP_FAITHFUL}))