#!/usr/bin/env python3
"""Build the KILL #2 review pages (stdlib only).

    python3 -B review/build.py        (run from the machine directory or anywhere)

Writes ../review.html and, in this folder: review.css, proof.html (submission proof.md rendered),
v.html (the kill .v with margin notes), tm7.html (SOMDCv6.v TM7 with line numbers), diff.html
(TM7 standalone copy vs the kill .v), notes.html, rocq-plan.html, rocq-log.html, readme.html, discord.html.

Every line number, count, hash and derivation shown on the pages is computed here from the source files
and asserted. The only hand-entered facts are the stage times in TIMELINE (each cites its source) and prose.
"""
import difflib
import hashlib
import html
import itertools
import json
import re
import subprocess
import sys
from pathlib import Path

ROOT = Path('[local working file]')
TM = '1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---'
TM7S = '1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---'
M = ROOT / 'machines' / TM
OUT = M / 'review'
VFILE = M / f'{TM}.v'
SUBV = M / 'submission' / f'{TM}.v'
SOM = ROOT / 'vendor/busycoq/verify/SOMDCv6.v'
TM7TOP = M / 'rocq-scratch/TM7_toplevel.v'
HOLD = ROOT / 'data/holdouts/2026-10-07_778.txt'


def rd(p):
    return Path(p).read_text(encoding='utf-8')


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


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


def fmt(n):
    return f'{n:,}'


FACT = {}   # computed facts used in prose; printed at the end for the record

# ============================================================== 1. the abstract relation R (proof.md section 2)
DIGC = {'L': '110', '0': '000', '1': '100'}


def inc(r):
    """+1 on the little-endian binary number of the 0/1 digits of r, L skipped; carry out appends a 1."""
    r = list(r)
    for i, d in enumerate(r):
        if d == 'L':
            continue
        if d == '0':
            r[i] = '1'
            return ''.join(r)
        r[i] = '0'
    return ''.join(r) + '1'


def cstep(tp, k, rest, ours=True, z=True):
    """One clause of R. Returns dict or None (no clause applies)."""
    if tp == 'hx':
        if not rest:
            return None
        d, r = rest[0], rest[1:]
        if d == 'L':
            return dict(cl='X1', rd='L', out='L', tp='hx', k=k + 1, rest=inc(r) if ours else r, inc=ours, done=False)
        if d == '0':
            return dict(cl='X2', rd='0', out='L', tp='hx', k=k + 1, rest=r, inc=False, done=False)
        return dict(cl='X3', rd='1', out='L', tp='h1', k=k, rest=r, inc=False, done=False)
    if not rest:
        if k == 0:
            return dict(cl='R0', rd='end', out='1', tp='h1', k=0, rest='', inc=False, done=True)
        if k % 2:
            return dict(cl='R1', rd='end', out='0', tp='h1', k=(k - 1) // 2, rest='', inc=False, done=False)
        return dict(cl='R2', rd='end', out='1', tp='h1', k=(k - 2) // 2, rest='', inc=False, done=False)
    if k == 0:
        if z and rest == '1':
            return dict(cl='Z1', rd='1', out='L', tp='h1', k=0, rest='', inc=False, done=True)
        if z and rest == '0':
            return dict(cl='Z0', rd='0', out='1', tp='h1', k=0, rest='', inc=False, done=True)
        return None
    d, r = rest[0], rest[1:]
    if d == 'L':
        return dict(cl='C1', rd='L', out='L', tp='hx', k=k, rest=inc(r) if ours else r, inc=ours, done=False)
    if d == '1':
        return dict(cl='C2', rd='1', out='L', tp='h1', k=k - 1, rest=r, inc=False, done=False)
    if k % 2:
        return dict(cl='C3', rd='0', out='0', tp='h1', k=(k - 1) // 2, rest=r, inc=False, done=False)
    return dict(cl='C4', rd='0', out='1', tp='h1', k=(k - 2) // 2, rest=r, inc=False, done=False)


def derive(tp, k, r, ours=True, z=True):
    """Full derivation of R(tp,k,r,_). Returns (steps, output or None)."""
    steps, out = [], ''
    while True:
        s = cstep(tp, k, r, ours, z)
        if s is None:
            steps.append(dict(cl='stuck', tp=tp, k=k, rest=r))
            return steps, None
        s['tp0'], s['k0'], s['rest0'] = tp, k, r
        steps.append(s)
        out += s['out']
        if s['done']:
            return steps, out
        tp, k, r = s['tp'], s['k'], s['rest']


def sweep(r, **kw):
    return derive('hx', 0, r, **kw)[1]


def Inv(tp, k, j, tq, q):
    if tp == 'hx' and tq == 'hx':
        return k <= q and j <= q
    if tp == 'h1' and tq == 'hx':
        return k + 1 <= q and j <= q
    if tp == 'h1' and tq == 'h1':
        return (j == 0 and 2 * k + 1 <= q) or (1 <= j and k + j <= q and 1 <= q)
    return False


def joint(r0):
    """The key lemma's induction, run on one word: first sweep over r0, second over its output."""
    r1 = sweep(r0)
    assert r1 is not None
    tp, k, rest, tq, q, srest, j = 'hx', 0, r0, 'hx', 0, r1, 0
    rows = []
    while True:
        K = k + j
        assert derive(tp, K, rest)[1] == srest, 'Lemma A link broken'
        assert Inv(tp, k, j, tq, q), 'Inv fails'
        if tp == 'h1' and (rest == '' or (k == 0 and rest in ('0', '1'))):
            s1 = cstep(tp, k, rest)
            fin_steps, fin = derive(tq, q, srest)
            assert fin is not None
            rows.append(dict(end=True, cl=s1['cl'], tp=tp, k=k, j=j, K=K, tq=tq, q=q, srest=srest,
                             fin=fin, fin_cls=[s['cl'] for s in fin_steps]))
            return r1, rows
        s1 = cstep(tp, k, rest)
        s2 = cstep(tq, q, srest)
        assert s1 and s2 and not s1['done'] and not s2['done']
        if s1['cl'] in ('C3', 'C4'):
            A = (K - 1) // 2 if K % 2 else (K - 2) // 2
            j2 = A - s1['k']
        else:
            j2 = j + 1
        rows.append(dict(end=False, n=len(rows) + 1, c1=s1['cl'], tp=tp, k=k, d1=rest[0], o1=s1['out'],
                         c2=s2['cl'], tq=tq, q=q, d2=srest[0], j=j, K=K))
        tp, k, rest, tq, q, srest, j = s1['tp'], s1['k'], s1['rest'], s2['tp'], s2['k'], s2['rest'], j2


# ============================================================== 2. the real machine
def parse_tm(s):
    t = {}
    for i, blk in enumerate(s.split('_')):
        for b in (0, 1):
            x = blk[3 * b:3 * b + 3]
            t[('ABCDEF'[i], b)] = None if x[2] == '-' else (int(x[0]), 1 if x[1] == 'R' else -1, x[2])
    return t


def S_word(tape, pos, st):
    """If the config is 0^inf 11 D> <r> 0^inf, return r (trailing 0 digits dropped), else None."""
    if st != 'D' or tape.get(pos - 1, 0) != 1 or tape.get(pos - 2, 0) != 1:
        return None
    if any(v for p, v in tape.items() if p < pos - 2):
        return None
    mx = max([p for p, v in tape.items() if v] + [pos])
    cells = [tape.get(p, 0) for p in range(pos, mx + 1)]
    while len(cells) % 3:
        cells.append(0)
    w = ''
    for i in range(0, len(cells), 3):
        c = ''.join(map(str, cells[i:i + 3]))
        if c not in ('110', '000', '100'):
            return None
        w += {'110': 'L', '000': '0', '100': '1'}[c]
    return w.rstrip('0')


def S_tape(r, pos=0):
    tape = {pos - 2: 1, pos - 1: 1}
    for i, d in enumerate(r):
        for j, c in enumerate(DIGC[d]):
            tape[pos + 3 * i + j] = int(c)
    return tape


def real_sweep(tms, r, cap=10 ** 6):
    """From S(r) with the head at cell 0, run to the first S config one cell further left."""
    t = parse_tm(tms)
    tape, pos, st = S_tape(r), 0, 'D'
    for n in range(1, cap):
        w, mv, nx = t[(st, tape.get(pos, 0))]
        tape[pos] = w
        pos += mv
        st = nx
        if pos == -1:
            s = S_word(tape, pos, st)
            if s is not None:
                return s, n
    raise RuntimeError('no boundary')


def run_rows(tms, tape, pos, st, nsteps=None, stop=None):
    """Simulate; return list of (step, state, head, tape copy, rule fired to get here)."""
    t = parse_tm(tms)
    rows = [(0, st, pos, dict(tape), None)]
    n = 0
    while True:
        if nsteps is not None and n >= nsteps:
            break
        sym = tape.get(pos, 0)
        rule = f'{st}{sym}'
        w, mv, nx = t[(st, sym)]
        tape[pos] = w
        pos += mv
        st = nx
        n += 1
        rows.append((n, st, pos, dict(tape), rule))
        if stop and stop(pos, st):
            break
    return rows


# ============================================================== 3. markdown -> HTML (headings, lists, tables, code, quotes)
def md_inline(s):
    codes = []

    def keep(m):
        codes.append(m.group(1))
        return f'\x00{len(codes) - 1}\x00'
    s = re.sub(r'`([^`]+)`', keep, s)
    s = esc(s)
    s = re.sub(r'\[([^\]]+)\]\(([^)\s]+)\)', lambda m: f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{m.group(2)}">{m.group(1)}</a>', s)
    s = re.sub(r'(?<![="])(https?://[^\s<)]+)', r'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/\1">\1</a>', s)
    s = re.sub(r'\*\*(.+?)\*\*', r'<strong>\1</strong>', s)
    s = re.sub(r'(?<![\w*])\*(?![\s*])(.+?)(?<![\s*])\*(?![\w*])', r'<em>\1</em>', s)
    s = re.sub('\x00(\\d+)\x00', lambda m: '<code>' + esc(codes[int(m.group(1))]) + '</code>', s)
    return s


def md_slug(text, used):
    m = re.match(r'^(\d+(?:\.\d+)*)\.?\s', text)
    base = 's' + m.group(1).replace('.', '-') if m else re.sub(r'[^a-z0-9]+', '-', text.lower()).strip('-') or 'h'
    sid, n = base, 2
    while sid in used:
        sid, n = f'{base}-{n}', n + 1
    used.add(sid)
    return sid


def md_cells(line):
    line = line.strip()
    if line.startswith('|'):
        line = line[1:]
    if line.endswith('|'):
        line = line[:-1]
    cells, cur, inb = [], '', False
    for ch in line:
        if ch == '`':
            inb = not inb
        if ch == '|' and not inb:
            cells.append(cur)
            cur = ''
        else:
            cur += ch
    cells.append(cur)
    return [c.strip() for c in cells]


def md(text):
    """Return (html, [(level, id, text)])."""
    lines = text.split('\n')
    out, toc, used = [], [], set()
    stack = []          # [indent, tag, li_has_text]
    para = []
    para_in_li_new = [False]

    def flush():
        if not para:
            return
        txt = md_inline(' '.join(x.strip() for x in para))
        if stack and not para_in_li_new[0]:
            out.append(txt)
            stack[-1][2] = True
        else:
            out.append(f'<p>{txt}</p>')
        para.clear()
        para_in_li_new[0] = False

    def close_to(indent):
        while stack and stack[-1][0] > indent:
            out.append(f'</li></{stack[-1][1]}>')
            stack.pop()

    i, blank = 0, False
    while i < len(lines):
        ln = lines[i]
        s = ln.strip()
        ind = len(ln) - len(ln.lstrip(' '))
        if not s:
            flush()
            blank = True
            i += 1
            continue
        if s.startswith('```'):
            flush()
            if ind == 0:
                close_to(-1)
            j = i + 1
            buf = []
            while j < len(lines) and not lines[j].strip().startswith('```'):
                buf.append(lines[j][ind:] if lines[j][:ind].strip() == '' else lines[j])
                j += 1
            out.append('<pre class="md">' + esc('\n'.join(buf)) + '</pre>')
            i, blank = j + 1, False
            continue
        m = re.match(r'^(#{1,6})\s+(.*)$', s)
        if m and ind == 0:
            flush()
            close_to(-1)
            lvl, t = len(m.group(1)), m.group(2)
            sid = md_slug(re.sub(r'[`*]', '', t), used)
            toc.append((lvl, sid, t))
            out.append(f'<h{lvl} id="{sid}">{md_inline(t)} <a class="hl" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#</span><span class="si">{sid}">#</a></h{lvl}>')
            i, blank = i + 1, False
            continue
        if s.startswith('|') and ind == 0:
            flush()
            close_to(-1)
            rows = []
            while i < len(lines) and lines[i].strip().startswith('|'):
                rows.append(lines[i])
                i += 1
            head = md_cells(rows[0])
            align = []
            body = rows[1:]
            if body and re.match(r'^\|?\s*:?-{3,}', body[0].strip()):
                align = ['r' if c.endswith(':') and not c.startswith(':') else '' for c in md_cells(body[0])]
                body = body[1:]
            t = ['<div class="tscroll"><table class="md"><thead><tr>']
            for n, c in enumerate(head):
                a = ' class="r"' if n < len(align) and align[n] == 'r' else ''
                t.append(f'<th{a}>{md_inline(c)}</th>')
            t.append('</tr></thead><tbody>')
            for r in body:
                t.append('<tr>')
                for n, c in enumerate(md_cells(r)):
                    a = ' class="r"' if n < len(align) and align[n] == 'r' else ''
                    t.append(f'<td{a}>{md_inline(c)}</td>')
                t.append('</tr>')
            t.append('</tbody></table></div>')
            out.append(''.join(t))
            blank = False
            continue
        if s.startswith('>') and ind == 0:
            flush()
            close_to(-1)
            buf = []
            while i < len(lines) and lines[i].strip().startswith('>'):
                buf.append(lines[i].strip()[1:].strip())
                i += 1
            out.append('<blockquote>' + md_inline(' '.join(buf)) + '</blockquote>')
            blank = False
            continue
        m = re.match(r'^(\s*)([-*]|\d+\.)\s+(.*)$', ln)
        if m:
            flush()
            tag = 'ol' if m.group(2)[0].isdigit() else 'ul'
            close_to(ind)
            if stack and stack[-1][0] == ind:
                if stack[-1][1] == tag:
                    out.append('</li>')
                else:
                    out.append(f'</li></{stack[-1][1]}>')
                    stack.pop()
                    out.append(f'<{tag}>')
                    stack.append([ind, tag, False])
            else:
                out.append(f'<{tag}>')
                stack.append([ind, tag, False])
            out.append('<li>')
            stack[-1][2] = False
            para.append(m.group(3))
            para_in_li_new[0] = False
            i, blank = i + 1, False
            continue
        # plain text
        if stack and ind > stack[-1][0]:
            if blank:
                flush()
                para_in_li_new[0] = True
            para.append(s)
        else:
            if stack and ind <= stack[0][0] and (blank or ind == 0):
                flush()
                close_to(-1)
            para.append(s)
        i, blank = i + 1, False
    flush()
    close_to(-1)
    return '\n'.join(out), toc


# ============================================================== 4. Coq highlighting
COQ_KW = set('''From Require Import Ltac Definition Fixpoint Inductive Notation Lemma Theorem Corollary Proof Qed
Open Close Scope match with end fun exists forall Eval compute in Unshelve Print Assumptions Module End as at level
using'''.split())
COQ_TAC = set('''intro intros induction destruct apply eapply rewrite cbn change constructor econstructor eexists
split repeat eauto auto lia subst inversion specialize remember pose epose proof gen f_equal symmetry reflexivity
discriminate contradiction try assert eassumption applys_eq unfold flia esc esx ec am cat3 tr1 wal tr2 follow10
es inc_nil all left right do clear vm_compute st inverts solve_v1 solve_v2 mid follow by'''.split())


def coq_tokens(src):
    """Yield (cls, text); cls in kw/tac/com/str/num/bul/None."""
    i, n = 0, len(src)
    bol = True
    while i < n:
        if src.startswith('(*', i):
            depth, j = 1, i + 2
            while j < n and depth:
                if src.startswith('(*', j):
                    depth += 1
                    j += 2
                elif src.startswith('*)', j):
                    depth -= 1
                    j += 2
                else:
                    j += 1
            yield 'com', src[i:j]
            i, bol = j, False
            continue
        c = src[i]
        if c == '"':
            j = src.index('"', i + 1) + 1
            yield 'str', src[i:j]
            i, bol = j, False
            continue
        if c == '\n':
            yield None, c
            i, bol = i + 1, True
            continue
        if c == ' ':
            j = i
            while j < n and src[j] == ' ':
                j += 1
            yield None, src[i:j]
            i = j
            continue
        if bol and c in '-+*' and i + 1 < n and src[i + 1] == ' ':
            yield 'bul', c
            i, bol = i + 1, False
            continue
        m = re.compile(r"[A-Za-z_][A-Za-z0-9_']*").match(src, i)
        if m:
            w = m.group(0)
            yield ('kw' if w in COQ_KW else 'tac' if w in COQ_TAC else None), w
            i, bol = m.end(), False
            continue
        m = re.compile(r'\d+').match(src, i)
        if m:
            yield 'num', m.group(0)
            i, bol = m.end(), False
            continue
        yield None, c
        i, bol = i + 1, False


def coq_lines(src):
    """List of per-line HTML strings (spans closed at each line end)."""
    lines, cur = [], []
    for cls, text in coq_tokens(src):
        parts = text.split('\n')
        for pi, p in enumerate(parts):
            if pi > 0:
                lines.append(''.join(cur))
                cur = []
            if p:
                cur.append(f'<span class="{cls}">{esc(p)}</span>' if cls else esc(p))
    lines.append(''.join(cur))
    return lines


# ============================================================== 5. sources, line lookup
VSRC = rd(VFILE)
VL = VSRC.split('\n')
if VL[-1] == '':
    VL = VL[:-1]
SOMSRC = rd(SOM)
SL = SOMSRC.split('\n')
NV = len(VL)
assert NV == 599, NV   # 597 until the comment-only header edit of 2026-10-10 (+2 header lines)


def find(lines, pat, lo=1, hi=None, nth=1):
    """1-based line number of the nth line in [lo,hi] matching regex pat."""
    hi = hi or len(lines)
    c = 0
    for n in range(lo, hi + 1):
        if re.search(pat, lines[n - 1]):
            c += 1
            if c == nth:
                return n
    raise KeyError(pat)


TM7_LO = find(SL, r'^Module TM7\.')
TM7_HI = find(SL, r'^End TM7\.')
TM8_LO = find(SL, r'^Module TM8\.')
FACT.update(tm7_lo=TM7_LO, tm7_hi=TM7_HI, tm8_lo=TM8_LO, tm7_len=TM7_HI - TM7_LO + 1)
assert (TM7_LO, TM7_HI) == (1626, 1871)
HDR_HI = TM7_LO - 1 if False else find(SL, r'^Module TM1\.') - 1   # shared header = lines before Module TM1


def rng(lines, a, b, lo=1, hi=None, nth=1):
    s = find(lines, a, lo, hi, nth)
    e = s if b is None else find(lines, b, s, hi)
    return s, e


def T7(a, b=None, nth=1):
    return rng(SL, a, b, TM7_LO, TM7_HI, nth)


def HD(a, b=None):
    return rng(SL, a, b, 1, 17)


def V(a, b=None, nth=1):
    return rng(VL, a, b, 1, NV, nth)


# ============================================================== 6. the .v, item by item
# (id, title, our range, proof.md anchor+label or None, src range in SOMDCv6 (text source) or None,
#  rel = (range, label) related TM7 text that is not the source, expected tag, plain-English note)
SPEC = [
    ('hdr', 'Header comment', V(r'^\(\* 1RB0RF', r'Closed under the global context\. \*\)$'), None, None, None, 'new',
     'Which machine, which template, the one-line idea, where the informal proof is, the AI-assistance line, and what '
     'was checked (busycoq commit, Coq version, the Print Assumptions result).'),
    ('imports', 'Imports', V(r'^From BusyCoq Require Import', r'^Require Import List\.'), None,
     HD(r'^From BusyCoq Require Import', r'^Require Import List\.'), None, 'copied',
     'The five Require lines of SOMDCv6.v\'s shared header.'),
    ('esc', 'Ltac esc', V(r'^Ltac esc :=', r'^  \(eapply sideRLs_c_spec'), None,
     HD(r'^Ltac esc :=', r'^  \(eapply sideRLs_c_spec'), None, 'copied',
     'Proves a concrete segment or side goal by running the machine (bounded computation).'),
    ('ec', 'Ltac ec', V(r'^Ltac ec :='), None, HD(r'^Ltac ec :='), None, 'copied',
     'Shorthand for econstructor, used to build R derivations.'),
    ('am', 'Ltac am', V(r'^Ltac am ', r'applys_eq \(segRLs_addmul_v2'), ('s3-1', '§3.1'),
     HD(r'^Ltac am ', r'applys_eq \(segRLs_addmul_v2'), None, 'copied',
     'Proves the halving pattern of a 0-digit (every 2 passes in, 1 out) from two small computed facts.'),
    ('tm', 'Definition tm', V(r'^Definition tm :='), None, T7(r'^Definition tm :='), None, 'adapted',
     'The machine. The only change from TM7\'s line is the string: A1 = 0RF instead of 0RC.'),
    ('arrows', 'Notations -->* and -->+', V(r'^Notation "c -->\*', r'^Notation "c -->\+'), None,
     T7(r'^Notation "c -->\*', r'^Notation "c -->\+'), None, 'copied',
     'Multi-step arrows for this tm.'),
    ('digits', 'Digits ld, d0, d1', V(r'^Notation ld :=', r'^Notation d1 :='), ('s1', '§1'),
     T7(r'^Notation ld :=', r'^Notation d1 :='), None, 'copied',
     'The three 3-cell digits: L = 110, 0 = 000, 1 = 100.'),
    ('w1ld', 'Notation w1ld', V(r'^Notation w1ld :='), ('s3-1', '§3.1 C1'), None, None, 'new',
     'The 4-cell word 1 110 (stray 1, then an L) that a drain pass meets in C1. Declared before Open Scope nat, '
     'where a list literal would be read as list nat.'),
    ('passes', 'Passes hR, hR\', hL, h, h\'', V(r'^Notation hR :=', r"^Notation h' :="), ('s1', '§1 Passes'),
     T7(r'^Notation hR :=', r"^Notation h' :="), None, 'copied',
     'h enters in state B and leaves in C (a drain pass, and also our +1 pass). h\' enters as 1 D> (the eater).'),
    ('RDH', 'Inductive RD, H', V(r'^Inductive RD :=', r'^Inductive H :='), ('s1', '§1'),
     T7(r'^Inductive RD :=', r'^Inductive H :='), None, 'copied',
     'Digit names LD, D0, D1, and the two modes: hx = eater, h1 = drain (with a stray 1 in front).'),
    ('toRC', 'Fixpoint toRC', V(r'^Fixpoint toRC', r'^end\.'), ('s1', '§1'),
     T7(r'^Fixpoint toRC', r'^end\.'), None, 'copied',
     'Turns a digit list into the right half-tape: the digits\' cells, then 0^inf.'),
    ('toHp', "Definition toH'", V(r"^Definition toH' x", r'^end\.'), ('s1', '§1'),
     T7(r"^Definition toH' x", r'^end\.'), None, 'copied',
     'The cell in front of the word: nothing for the eater, the stray 1 for the drain.'),
    ('toH', 'Definition toH', V(r'^Definition toH x', r'^end\.'), ('s1', '§1'),
     T7(r'^Definition toH x', r'^end\.'), None, 'copied',
     'The first pass of each mode: the eater pass h\' for hx, nothing extra for h1.'),
    ('Inc', 'Inductive Inc', V(r'^\(\* one h pass', r'^\| Inc_ld'), ('s2', '§2 Inc'), None, None, 'new',
     'Inc r r\': r\' is r + 1, reading the 0/1 digits as a little-endian binary number and skipping L. '
     'Clauses in proof.md\'s names: Inc_nil = I4, Inc_d0 = I2, Inc_d1 = I1 (carry), Inc_ld = I3.'),
    ('RIncs', 'Inductive RIncs (the sweep relation R)', V(r'^Inductive RIncs', r'^\.$'), ('s2', '§2 R'),
     T7(r'^Inductive RIncs', r'^\.$'), None, 'adapted',
     'R(mode, k, r, r\'): 12 clauses. 8 are TM7\'s text. X1 (hx_ld) and C1 (h1_ld) gain an Inc premise and '
     'continue on the incremented rest. Z1 and Z0 are new zero-pass clauses.'),
    ('ltacs', 'Ltacs cat3, tr1, wal, tr2', V(r'^Ltac cat3 :=', r'^  eapply sideRLs_trans; \[esx \| \]\.'), None,
     T7(r'^Ltac cat3 :=', r'^  eapply sideRLs_trans; \[esx \| \]\.'), None, 'copied',
     'cat3 peels one 3-cell digit off the side; tr1/tr2 split off a first pass; wal pushes k identical passes '
     'through a fixed segment.'),
    ('z1_eq', 'Lemma z1_eq', V(r'^Lemma z1_eq', r'^Qed\.'), ('s3-1', '§3.1 Z1, Z0'), None, None, 'new',
     'As tapes, 1 100 0^inf = 110 0^inf. This identity is all that clause Z1 says.'),
    ('z0_eq', 'Lemma z0_eq', V(r'^Lemma z0_eq', r'^Qed\.'), ('s3-1', '§3.1 Z1, Z0'), None, None, 'new',
     'As tapes, 1 000 0^inf = 100 0^inf: the identity behind Z0.'),
    ('Inc_spec', 'Lemma Inc_spec', V(r'^Lemma Inc_spec', r'^Qed\.'), ('s3-1', '§3.1 Inc_spec'), None, None, 'new',
     'Machine fact: one h pass over the cells of r leaves the cells of r + 1. One computed segment fact per digit.'),
    ('seg_hx_ld', 'Lemma seg_hx_ld', V(r'^Lemma seg_hx_ld', r'^Qed\.'), ('s3-1', '§3.1 X1'), None,
     (T7(r'^  - cat3; tr1; wal\.'), 'TM7 does this L cell inline in RIncs_spec bullet 1'), 'new',
     'Eater enters an L: the cells 110 stay 110, and the passes sent on to the right become h (the +1 pass), '
     'then h\', then k+1 drain passes. In TM7 the leading h is absent.'),
    ('seg_h1_ld', 'Lemma seg_h1_ld', V(r'^Lemma seg_h1_ld', r'^Qed\.'), ('s3-1', '§3.1 C1'), None,
     (T7(r'^  - rewrite lpow_add,app_assoc\.', r'^    tr1; wal\.'),
      'TM7 does this inline in RIncs_spec bullet 4'), 'new',
     'A drain pass meets 1 110: the same output shape, h ++ h\' ++ h^(1+k).'),
    ('RIncs_spec', 'Lemma RIncs_spec', V(r'^Lemma RIncs_spec', r'^Qed\.'), ('s3-1', '§3.1'),
     T7(r'^Lemma RIncs_spec', r'^Qed\.'), None, 'adapted',
     'Soundness: every R derivation is an exact run of the machine at the pass level (sideRLs). One bullet per '
     'clause. Bullets 1 and 4 (X1, C1) chain seg_*_ld with Inc_spec; the last two (Z1, Z0) rewrite with z1_eq/z0_eq; '
     'the other 8 are TM7\'s.'),
    ('Inc_total', 'Lemma Inc_total', V(r'^Lemma Inc_total', r'^Qed\.'), ('s3-3', '§3.3 table'), None, None, 'new',
     'Every word has a +1.'),
    ('Inc_fun', 'Lemma Inc_fun', V(r'^Lemma Inc_fun', r'^Qed\.'), ('s3-3', '§3.3 table'), None, None, 'new',
     'The +1 is unique. The only functionality fact the domain proof uses.'),
    ('RIncs_eqk', 'Lemma RIncs_eqk', V(r'^Lemma RIncs_eqk', r'^Proof\. intros; subst; auto\. Qed\.'), None,
     None, None, 'new',
     'Helper: change the count of an R fact to an equal number, so clauses with counts like 1+k*2 apply after lia.'),
    ('inc_nil', 'Ltac inc_nil', V(r'^Ltac inc_nil :=', r'^  end\.'), None, None, None, 'new',
     'Helper: an Inc [] _ hypothesis can only be Inc [] [D1]; invert it.'),
    ('RIncs_Inc', 'Lemma RIncs_Inc (Lemma A)', V(r'^\(\* proof\.md Lemma A', r'^Qed\.'), ('s3-3', '§3.3 Lemma A'),
     None, None, 'new',
     'Lemma A: one more pass after a sweep\'s k passes = +1 on its output. Each clause maps to the same clause with '
     'count k+1, except C3/C4 swap on a carry, R0/R1/R2 shift, Z1 becomes C2 and Z0 becomes C3.'),
    ('RIncs_nxt_1', 'Lemma RIncs_nxt_1 (Total_1)', V(r'^Lemma RIncs_nxt_1', r'^Qed\.'), ('s3-3', '§3.3 Total_1'),
     T7(r'^Lemma RIncs_nxt_1', r'^Qed\.'), None, 'copied',
     'A drain with any count q at the right end always finishes.'),
    ('End_1', 'Lemma End_1', V(r'^Lemma End_1', r'^Qed\.'), ('s3-3', '§3.3 End_1'), None,
     (T7(r'^  \{', r'^  \}'), 'TM7 handles r = [] inside RIncs_nxt by an inner induction on k'), 'new',
     'If the right end with count m wrote w, then a drain arriving at w with any q >= m reads w to the end.'),
    ('End_x', 'Lemma End_x', V(r'^Lemma End_x', r'^Qed\.'), ('s3-3', '§3.3 End_x'), None,
     (T7(r'^  \{', r'^  \}'), 'TM7 handles r = [] inside RIncs_nxt by an inner induction on k'), 'new',
     'The same for an eater arriving at w: any q with m <= 2q+2 suffices.'),
    ('inv', 'Inversion helpers (7)', V(r'^\(\* inversion helpers', r'^Qed\.', nth=1), ('s3-3', '§3.3 proof'),
     None, None, 'new', None),   # end fixed below (the Qed of inv_z1)
    ('Inv', 'Definition Inv', V(r'^\(\* proof\.md section 3\.3', r'^  end\.'), ('s3-3', '§3.3 Inv'), None,
     (T7(r"^  match tp,tp' with", r'^  end ->'), 'TM7\'s RIncs_nxt condition'), 'new',
     'How many passes the second sweep needs, given the first sweep\'s mode and count (tp, k), the j pending +1s, '
     'and the second\'s mode and count (tq, q). With j = 0 it is exactly TM7\'s condition.'),
    ('key', "Lemma key (proof.md's RIncs_nxt')", V(r'^Lemma key ', r'^Qed\.'), ('s3-3', '§3.3 Key lemma'), None,
     (T7(r'^Lemma RIncs_nxt ', r'^Qed\.'), 'replaces TM7\'s RIncs_nxt'), 'new',
     'The domain lemma. If the first sweep is defined on r, and a second sweep reads its output after j pending '
     '+1s with enough passes (Inv), the second sweep is defined too. Induction on the first derivation: one bullet '
     'per clause (12).'),
    ('domain', 'Lemma domain', V(r'^Lemma domain ', r'^Qed\.'), ('s5', '§5'), None,
     (T7(r'^  pose proof I1 as I2\.', r'^  2: lia\.'), 'TM7 calls RIncs_nxt inline in nonhalt'), 'new',
     'The instance used: a sweep\'s output can be swept again (key at k = j = q = 0).'),
    ('lh', 'Notation lh', V(r'^Notation lh :='), ('s1', '§1 Family'), T7(r'^Notation lh :='), None, 'copied',
     'The left part 0^inf 1: everything left of the wall\'s second 1.'),
    ('Sp', "Definition S'", V(r"^Definition S' r :=", r'^  lh \{\{\{'), ('s1', '§1 Family'),
     T7(r"^Definition S' r :=", r'^  lh \{\{\{'), None, 'copied',
     'The boundary configuration S(r) = 0^inf 11 D> <r> 0^inf.'),
    ('BigStep', 'Lemma BigStep', V(r'^Lemma BigStep', r'^Qed\.'), ('s3-2', '§3.2'),
     T7(r'^Lemma BigStep', r'^Qed\.'), None, 'copied',
     'One sweep: R(hx,0,r,r\') gives S(r) -->+ S(r\'). RIncs_spec supplies the pass, sideRLs_1 and follow10 run it, '
     'es does the 3-step wall.'),
    ('start', 'Lemma start', V(r'^Lemma start:', r'^Proof\. esx\. Qed\.'), ('s4', '§4'), None,
     (T7(r"^  eapply multistep_nonhalt with \(c':=S' \[D1\]\)\.", r'^  1: esx\.'), 'TM7 goes to S\'[D1] inline'),
     'new',
     'The blank tape reaches S(L1) (step 16), by computation. TM7 stops one sweep earlier, at S(1) (step 5).'),
    ('nonhalt', 'Lemma nonhalt (the theorem)', V(r'^Lemma nonhalt:', r'^Qed\.'), ('s5', '§5'),
     T7(r'^Lemma nonhalt:', r'^Qed\.'), None, 'adapted',
     'multistep_nonhalt to S(L1), then progress_nonhalt_cond with P r := exists r\', R(hx,0,r,r\'): BigStep makes '
     'the step and domain keeps P. Differs from TM7 in the start, a hand-built witness for P, and the domain call.'),
    ('table', 'Rule-table comment', V(r'^\(\*$', r'^\*\)$', nth=1), ('s2', '§2'), None, None, 'new',
     'The rule table in the comment block that busycoq proof files end with.'),
]
# fix the inversion-helper block end: from its comment to the Qed of inv_z1
_inv_s = find(VL, r'^\(\* inversion helpers')
_inv_e = find(VL, r'^Qed\.', find(VL, r'^Lemma inv_z1'))
SPEC = [(a, b, (_inv_s, _inv_e) if a == 'inv' else c, d, e, f, g,
         'What an R fact must look like given its first digit, one lemma per case. inv_h1_d0 has three outcomes '
         '(odd count, even count, or Z0). TM7 used inverts inline instead.' if a == 'inv' else h)
        for (a, b, c, d, e, f, g, h) in SPEC]
# rule-table comment is the LAST (* line
_tab_s = max(n for n in range(1, NV + 1) if VL[n - 1] == '(*')
SPEC = [(a, b, (_tab_s, NV) if a == 'table' else c, d, e, f, g, h) for (a, b, c, d, e, f, g, h) in SPEC]


def text_of(lines, r):
    return [x.rstrip() for x in lines[r[0] - 1:r[1]]]


ITEMS = []
for (iid, title, vr, pref, src, rel, expect, note) in SPEC:
    if src is None:
        tag = 'new'
    else:
        tag = 'copied' if text_of(VL, vr) == text_of(SL, src) else 'adapted'
    assert tag == expect, (iid, tag, expect)
    ITEMS.append(dict(id=iid, title=title, vr=vr, pref=pref, src=src, rel=rel, tag=tag, note=note))
# no overlaps, in order
for a, b in zip(ITEMS, ITEMS[1:]):
    assert a['vr'][1] < b['vr'][0], (a['id'], b['id'])
ITEM = {it['id']: it for it in ITEMS}
covered = set()
for it in ITEMS:
    covered.update(range(it['vr'][0], it['vr'][1] + 1))
GLUE = [n for n in range(1, NV + 1) if n not in covered]
for n in GLUE:   # everything outside an item is blank or a scope / section line
    assert VL[n - 1].strip() in ('', 'Open Scope nat.', 'Open Scope sym.', 'Close Scope sym.') or \
        VL[n - 1].startswith('(* ----------'), (n, VL[n - 1])

TAGLINES = {t: sum(it['vr'][1] - it['vr'][0] + 1 for it in ITEMS if it['tag'] == t) for t in ('copied', 'adapted', 'new')}
TAGLINES['glue'] = len(GLUE)
GLUE_KIND = dict(blank=sum(1 for n in GLUE if not VL[n - 1].strip()), scope=sum(1 for n in GLUE if 'Scope' in VL[n - 1]),
                 section=sum(1 for n in GLUE if VL[n - 1].startswith('(* ----------')))
assert sum(GLUE_KIND.values()) == len(GLUE)
assert sum(TAGLINES.values()) == NV
TAGCOUNT = {t: sum(1 for it in ITEMS if it['tag'] == t) for t in ('copied', 'adapted', 'new')}
NEW33 = sum(it['vr'][1] - it['vr'][0] + 1 for it in ITEMS if it['tag'] == 'new' and it['id'] in
            ('Inc_total', 'Inc_fun', 'RIncs_eqk', 'inc_nil', 'RIncs_Inc', 'End_1', 'End_x', 'inv', 'Inv', 'key', 'domain'))

# per-line change marks inside adapted items (lines not matched in TM7's text)
CHANGED = set()
for it in ITEMS:
    if it['tag'] != 'adapted':
        continue
    a, b = text_of(SL, it['src']), text_of(VL, it['vr'])
    sm = difflib.SequenceMatcher(None, a, b, autojunk=False)
    keep = set()
    for blk in sm.get_matching_blocks():
        keep.update(range(blk.b, blk.b + blk.size))
    for i in range(len(b)):
        if i not in keep and b[i].strip():
            CHANGED.add(it['vr'][0] + i)

# RIncs clauses: compare each constructor with TM7's
def constructors(lines, r):
    out, cur, name = {}, [], None
    for n in range(r[0], r[1] + 1):
        x = lines[n - 1]
        m = re.match(r'^\| (\w+)', x)
        if m:
            if name:
                out[name] = cur
            name, cur = m.group(1), [(n, x.strip())]
        elif name and x.strip() and x.strip() != '.':
            cur.append((n, x.strip()))
    if name:
        out[name] = cur
    return out


OUR_C = constructors(VL, ITEM['RIncs']['vr'])
TM7_C = constructors(SL, ITEM['RIncs']['src'])
assert len(OUR_C) == 12 and len(TM7_C) == 10
CL_TAG = {}
for nm, body in OUR_C.items():
    if nm not in TM7_C:
        CL_TAG[nm] = 'new'
    else:
        CL_TAG[nm] = 'copied' if [t for _, t in body] == [t for _, t in TM7_C[nm]] else 'adapted'
assert CL_TAG == {'RIncs_hx_ld': 'adapted', 'RIncs_hx_d1': 'copied', 'RIncs_hx_d0': 'copied',
                  'RIncs_h1_ld': 'adapted', 'RIncs_h1_d1': 'copied', 'RIncs_h1_d0_0': 'copied',
                  'RIncs_h1_d0_1': 'copied', 'RIncs_h1_rh_0': 'copied', 'RIncs_h1_rh_1': 'copied',
                  'RIncs_h1_rh_2': 'copied', 'RIncs_h1_z1': 'new', 'RIncs_h1_z0': 'new'}, CL_TAG
CLINE = {nm: body[0][0] for nm, body in OUR_C.items()}
CLINE7 = {nm: body[0][0] for nm, body in TM7_C.items()}

# RIncs_spec bullets: which are TM7's text
def bullets(lines, r):
    out, cur = [], None
    for n in range(r[0], r[1] + 1):
        x = lines[n - 1]
        if re.match(r'^  - ', x):
            if cur:
                out.append(cur)
            cur = [(n, x.strip())]
        elif cur is not None and x.startswith('    '):
            cur.append((n, x.strip()))
        elif cur is not None and x.strip() == 'Qed.':
            out.append(cur)
            cur = None
    return out


OB = bullets(VL, ITEM['RIncs_spec']['vr'])
TB = bullets(SL, ITEM['RIncs_spec']['src'])
assert len(OB) == 12 and len(TB) == 10
SAME_B = [i for i in range(10) if [t for _, t in OB[i]] == [t for _, t in TB[i]]]
assert SAME_B == [1, 2, 4, 5, 6, 7, 8, 9], SAME_B   # 0-based: bullets 2,3,5..10 are TM7's
FACT['spec_same'] = len(SAME_B)

# repeated text inside key (reviewability)
KEYR = ITEM['key']['vr']


def block_after(pat, n_lines):
    s = find(VL, pat, KEYR[0], KEYR[1])
    return s, [x.rstrip() for x in VL[s:s + n_lines]]


def case_range(name):
    s = find(VL, r'^  - \(\* ' + re.escape(name) + r' \*\)', KEYR[0], KEYR[1])
    nxt = [n for n in range(s + 1, KEYR[1]) if re.match(r'^  - \(\* ', VL[n - 1])]
    e = (nxt[0] - 1) if nxt else KEYR[1] - 1
    return s, e


KCASES = {c: case_range(c) for c in ['hx_ld', 'hx_d1', 'hx_d0', 'h1_ld', 'h1_d1', 'h1_d0_0', 'h1_d0_1',
                                     'rh_0', 'rh_1', 'rh_2', 'z1', 'z0']}


def body(c):
    s, e = KCASES[c]
    return [x.rstrip() for x in VL[s:e]]       # without the "- (* name *)" line


assert body('h1_d0_0') == body('h1_d0_1')
assert body('rh_0') == body('rh_1') == body('rh_2')
d = [i for i, (a, b) in enumerate(zip(body('hx_d1'), body('hx_d0'))) if a != b]
assert len(body('hx_d1')) == len(body('hx_d0')) and len(d) == 1
FACT['key_len'] = KEYR[1] - KEYR[0] + 1
FACT['dup_d0'] = len(body('h1_d0_0'))
FACT['dup_rh'] = len(body('rh_0'))
FACT['dup_hx'] = len(body('hx_d1'))

# ============================================================== 7. facts from other files
NOTES = rd(M / 'notes.md')
PROOF_W = rd(M / 'proof.md')
PROOF_S = rd(M / 'submission/proof.md')
CKTXT = rd(M / 'submission/check_kill.txt')
README = rd(M / 'submission/README.md')
DISCORD = rd(M / 'submission/discord.md')
PLAN = rd(M / 'rocq-plan.md')
RLOG = rd(M / 'rocq/log.md')
LEDGER = rd(ROOT / 'reports/overnight-ledger.md')
TARGET = rd(ROOT / 'reports/targeting.md')
OBS = json.loads(rd(M / 'observe.json'))
STATUSJ = json.loads(rd(M / 'status.json'))

V_SHA = sha(VFILE)
assert V_SHA == sha(SUBV) == 'e434537eca67d99fd1b0e7a769808ac3fc220425beb684c3a401b74652c1b076'
# the .v as killed and audited 04:45-04:51, before the comment-only header edit (repo-local paths out, 2026-10-10)
V_SHA0 = '3b29083b31f348bb3172c47b7e51a389b324165d9c38a073a56d9f9a760a651d'
assert f'"sha256":"{V_SHA}"' in CKTXT and 'RESULT: PASS -- this is a kill' in CKTXT
CKJ = json.loads(CKTXT.split('JSON: ', 1)[1].strip())
assert CKJ['result'] == 'PASS' and len(CKJ['checks']) == 17 and all(c['status'] == 'PASS' for c in CKJ['checks'])
FACT.update(ck_checked=CKJ['checked_at'], ck_compile=CKJ['compile_seconds'], ck_coqchk=CKJ['coqchk_seconds'],
            ck_assump=len(CKJ['assumptions']), ck_head=CKJ['framework_head'])
RR = rd(OUT / 'check_kill_rerun.txt')   # check_kill re-run for this page (saved output)
RRJ = json.loads(RR.split('JSON: ', 1)[1].split('\n')[0])
RRWALL = float(re.search(r'^wall ([\d.]+)s$', RR, re.M).group(1))   # /usr/bin/time line appended to the saved output
assert RRJ['result'] == 'PASS' and RRJ['sha256'] == V_SHA and len(RRJ['checks']) == 17 and all(c['status'] == 'PASS' for c in RRJ['checks'])
FACT.update(rr_checked=RRJ['checked_at'], rr_compile=RRJ['compile_seconds'], rr_coqchk=RRJ['coqchk_seconds'], rr_assump=len(RRJ['assumptions']))
# the audit agent's check_kill --json output (copied from its scratchpad, which is temporary): the 4th PASS in Fig A
AUJ = json.loads(rd(OUT / 'check_kill_audit.json'))
assert AUJ['result'] == 'PASS' and AUJ['sha256'] == V_SHA0 and len(AUJ['checks']) == 17 and all(c['status'] == 'PASS' for c in AUJ['checks'])
assert AUJ['checked_at'] == '2026-10-10T11:46:58Z' and AUJ['assumptions'] == []
HL = rd(HOLD).split('\n')
HLINE = [i + 1 for i, x in enumerate(HL) if x == TM]
assert HLINE == [301] and len([x for x in HL if x]) == 778
LN_TM = find(VL, r'^Definition tm := Eval compute in \(TM_from_str "' + re.escape(TM) + r'"\)\.$')
LN_NH = find(VL, r'^Lemma nonhalt: ~halts tm c0\.$')
assert (LN_TM, LN_NH) == (27, 560)   # (25, 558) before the header edit
assert len(rd(TM7TOP).split('\n')) - 1 == 261
assert rd(TM7TOP).split('\n')[:-1] == SL[0:17] + SL[TM7_LO:TM7_HI - 1]
assert STATUSJ['status'] == 'KILLED_NONHALT'
m = re.search(r'```text\n(.*?)\n```', DISCORD, re.S)
FACT['discord_chars'] = len(m.group(1))
assert FACT['discord_chars'] == 1371 and m.group(1).count('<LINK>') == 1
FACT['discord_chars_nolink'] = len(m.group(1).replace('<LINK>', ''))
assert '1,371 characters before the link' in DISCORD and 'a draft of 1,371 characters plus `<LINK>`' in NOTES
assert '208/208' in NOTES and '115 of the 208' in NOTES and '1/208' in NOTES
assert 'Verdict: sound; 5 minor gaps' in PROOF_W
assert "proof.md's case table (§3.3) matched the Coq cases one to one" in RLOG
assert 'compiles in 3.8 s' in PLAN and 'RESULT: PASS' in PLAN
assert '04:52 | KILL #2 verified (check_kill PASS x3: formalizer, audit, orchestrator)' in LEDGER
assert '| 2 | `1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---` | Bell eats counter |' in TARGET
assert 'Formalizer, 11:45:36Z' in NOTES and 'Fresh human-readable run for the submission, 11:48:20Z' in NOTES
assert len(OBS['history']['rows']) == 40
FIG1 = [d for d in OBS['diagrams'] if d['png'] == 'img/eat_pair.png'][0]
assert FIG1['window'] == 'cells -4..24, 1 px = 1/12 cell (cell 12 px wide, step 8 px tall)', FIG1['window']
FIG1_WINDOW = 'cells -4..24; 1 cell = 12 px wide, 1 step = 8 px tall'
FIG2 = [d for d in OBS['diagrams'] if d['png'] == 'img/sweep_pair.png'][0]

# ============================================================== 8. derivations used in the figures (all asserted)
W0 = 'LLLL1L1'
OURS_ST, OURS_OUT = derive('hx', 0, W0)
TM7_ST, TM7_OUT = derive('hx', 0, W0, ours=False)
assert OURS_OUT == 'L' * 9 + '111' and TM7_OUT == 'L' * 7 + '101'
assert real_sweep(TM, W0) == ('L' * 9 + '111', 421) and real_sweep(TM7S, W0) == ('L' * 7 + '101', 237)
CE0 = 'LLLL10LL1L1'
CE1 = sweep(CE0)
assert CE1 == 'LLLLL1LLLLLLL111'
CE1_NOZ_STEPS, CE1_NOZ = derive('hx', 0, CE1, z=False)
CE2 = sweep(CE1)
assert CE1_NOZ is None and CE2 == 'LLLLLLLLLLLLLL011L'
assert sweep(CE0, z=False) == CE1
assert real_sweep(TM, CE0)[0] == CE1 and real_sweep(TM, CE1)[0] == CE2
FACT['ce_steps'] = (real_sweep(TM, CE0)[1], real_sweep(TM, CE1)[1])
JW_R1, JW = joint(CE0)
assert JW_R1 == CE1 and JW[-1]['end'] and 'Z1' in JW[-1]['fin_cls']

# exhaustive domain closure, words of <= 11 digits (proof.md section 3.3 / 7)
dz = dn = fz = fn = 0
for n in range(12):
    for w in itertools.product('L01', repeat=n):
        r = ''.join(w)
        a = sweep(r)
        if a is not None:
            dz += 1
            fz += sweep(a) is None
        b = sweep(r, z=False)
        if b is not None:
            dn += 1
            fn += sweep(b, z=False) is None
assert (dz, fz, dn, fn) == (76738, 0, 71865, 170), (dz, fz, dn, fn)
FACT.update(dom_z=dz, dom_noz=dn, fail_noz=fn)

# from blank: boundary configs at steps 5, 16, 91 (left record + 2), head one cell further left each time
BLANK = run_rows(TM, {}, 0, 'A', nsteps=91)
BOUND = []
for (n, st, pos, tape, rule) in BLANK:
    w = S_word(tape, pos, st)
    if w is not None and (not BOUND or pos == BOUND[-1][2] - 1):
        BOUND.append((n, w, pos, tape))
assert [(b[0], b[1], b[2]) for b in BOUND] == [(5, '1', 1), (16, 'L1', 0), (91, 'LLL11', -1)], BOUND
WALLROWS = BLANK[13:17]
assert [r[4] for r in WALLROWS[1:]] == ['C1', 'D0', 'D0'] and WALLROWS[0][1] == 'C' and WALLROWS[0][2] == -1
assert sweep('1') == 'L1' and sweep('L1') == 'LLL11'
WIT = derive('hx', 0, 'L1')
assert WIT[1] == 'LLL11' and [s['cl'] for s in WIT[0]] == ['X1', 'X2', 'X3', 'R2', 'R0']

# one +1 pass on the real machine: 1 B> <1 1 L 0> 0^inf -> <C <0 0 L 1>, 6j+1 steps, no A1
X = '11L0'
ptape = {-1: 1}
for i, dg in enumerate(X):
    for j2, c in enumerate(DIGC[dg]):
        ptape[3 * i + j2] = int(c)
PASS = run_rows(TM, ptape, 0, 'B', stop=lambda pos, st: pos == -1)
jdig = X.index('0')
assert len(PASS) - 1 == 6 * jdig + 1 == 19
assert PASS[-1][1] == 'C' and not any(r[4] == 'A1' for r in PASS[1:])
endcells = ''.join(str(PASS[-1][3].get(p, 0)) for p in range(0, 12))
assert endcells == ''.join(DIGC[d] for d in inc(X)) and inc(X) == '00L1'

# ============================================================== 9. HTML helpers
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);--bad:#c4372f;
 --caution:#a86b00;--code:#f0efea;--good:#2c7a4b;--good-weak:rgba(44,122,75,.10);
 --s1:#2a78d6;--s2:#eb6834;--s0:#9b998f;--s1w:rgba(42,120,214,.13);--s2w:rgba(235,104,52,.14);--s0w:rgba(155,153,143,.16);
 --c1:#ffffff;--c0:#161616;--cellb:#8f8d85;--head:#d0312d;
 --kw:#7a3e9d;--tac:#2457c5;--com:#7a786f;--str:#2c7a4b;--num:#9a5f00;--chg:rgba(235,104,52,.16)}
@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);--bad:#ee6b64;
 --caution:#f0b43c;--code:#272725;--good:#6cc28c;--good-weak:rgba(108,194,140,.12);
 --s1:#3987e5;--s2:#d95926;--s0:#77756e;--s1w:rgba(57,135,229,.20);--s2w:rgba(217,89,38,.22);--s0w:rgba(119,117,110,.22);
 --c1:#f4f4f2;--c0:#050505;--cellb:#6c6a63;--head:#ff5f57;
 --kw:#c79bf0;--tac:#82a8f0;--com:#98968e;--str:#6cc28c;--num:#f0b43c;--chg:rgba(217,89,38,.22)}}
: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);--bad:#ee6b64;
 --caution:#f0b43c;--code:#272725;--good:#6cc28c;--good-weak:rgba(108,194,140,.12);
 --s1:#3987e5;--s2:#d95926;--s0:#77756e;--s1w:rgba(57,135,229,.20);--s2w:rgba(217,89,38,.22);--s0w:rgba(119,117,110,.22);
 --c1:#f4f4f2;--c0:#050505;--cellb:#6c6a63;--head:#ff5f57;
 --kw:#c79bf0;--tac:#82a8f0;--com:#98968e;--str:#6cc28c;--num:#f0b43c;--chg:rgba(217,89,38,.22)}
*{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}
p{margin:6px 0}
.muted{color:var(--muted)}.ink2{color:var(--ink2)}
.wrap{max-width:1240px;margin:0 auto;padding:14px 24px 60px}
header.top{display:flex;flex-wrap:wrap;align-items:center;gap:6px 14px;padding-bottom:10px;border-bottom:1px solid var(--line)}
.rank{font-weight:700;font-size:16px;color:var(--muted)}
.tmname{font:600 15px/1.3 ui-monospace,"Cascadia Code",Consolas,monospace;background:none;padding:0;word-break:break-all}
.cls{font-size:13.5px;color:var(--ink2)}
.links{display:flex;flex-wrap:wrap;gap:2px 14px;font-size:13.5px;margin-left:auto}
.state{display:flex;flex-wrap:wrap;align-items:baseline;gap:4px 12px;margin-top:10px;padding:7px 12px;border-radius:8px;
 background:var(--surface);border:1px solid var(--line);border-left:4px solid var(--good);font-size:14px}
.gtag{font-weight:700;color:var(--good)}
nav.sec{position:sticky;top:0;z-index:5;background:var(--page);border-bottom:1px solid var(--line);margin:0 -24px;padding:6px 24px;
 display:flex;flex-wrap:wrap;gap:4px 18px;font-size:13.5px}
nav.sec a{color:var(--ink2);font-weight:600}nav.sec a:hover{color:var(--accent)}
nav.sec .sub{color:var(--muted);font-weight:400}
h2.sh{font-size:21px;margin:34px 0 4px;letter-spacing:-.01em;scroll-margin-top:44px}
h2.sh .L{display:inline-block;min-width:28px;color:var(--accent)}
h3{font-size:16px;margin:22px 0 6px;scroll-margin-top:44px}
.lead{color:var(--ink2);max-width:920px;margin:2px 0 12px}
.steps{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:10px;margin:14px 0 6px}
.step{background:var(--surface);border:1px solid var(--line);border-radius:10px;padding:10px 12px;font-size:13.5px}
.step b{display:block;font-size:14.5px;margin-bottom:2px}.step .n{color:var(--accent);font-weight:700;margin-right:6px}
.callout{background:var(--surface);border:1px solid var(--line);border-left:4px solid var(--accent);border-radius:8px;padding:9px 13px;margin:12px 0;font-size:14px;max-width:1000px}
.callout.good{border-left-color:var(--good)}.callout.warn{border-left-color:var(--caution)}
table.t{border-collapse:collapse;width:100%;font-size:13.5px;background:var(--surface);border:1px solid var(--line);border-radius:8px;overflow:hidden}
table.t th{text-align:left;font-weight:650;color:var(--ink2);background:var(--sunk);padding:6px 9px;border-bottom:1px solid var(--line);font-size:12.5px;white-space:nowrap}
table.t td{padding:6px 9px;border-bottom:1px solid var(--line);vertical-align:top}
table.t tr:last-child td{border-bottom:0}
table.t td.r,table.t th.r{text-align:right;font-variant-numeric:tabular-nums}
table.t tr.grp td{background:var(--sunk);font-weight:650;color:var(--ink2);font-size:12.5px;letter-spacing:.03em;text-transform:uppercase}
.tscroll{overflow-x:auto;max-width:100%}
.chip{display:inline-flex;align-items:center;gap:4px;border:1px solid var(--line);background:var(--surface);border-radius:999px;padding:0 8px;font-size:12px;white-space:nowrap;color:var(--ink)}
.tag{display:inline-block;border-radius:4px;padding:0 6px;font-size:11.5px;font-weight:650;white-space:nowrap;border:1px solid}
.tag.copied{color:var(--ink2);border-color:var(--s0);background:var(--s0w)}
.tag.adapted{color:var(--ink);border-color:var(--s1);background:var(--s1w)}
.tag.new{color:var(--ink);border-color:var(--s2);background:var(--s2w)}
.who{display:inline-block;font-size:11.5px;border-radius:4px;padding:0 5px;margin:1px 2px 1px 0;background:var(--sunk);color:var(--ink2);white-space:nowrap}
figure.fig{margin:16px 0 22px;background:var(--surface);border:1px solid var(--line);border-radius:10px;padding:12px 14px}
figure.fig>figcaption{font-weight:650;font-size:15px;margin-bottom:6px}
figure.fig>figcaption .fno{color:var(--accent);margin-right:6px}
.flabel{margin-top:10px;padding-top:7px;border-top:1px dashed var(--line);font-size:12.5px;color:var(--ink2);display:flex;flex-wrap:wrap;gap:2px 16px}
.flabel b{color:var(--muted);font-weight:650;margin-right:4px}
.why{font-size:13.5px;color:var(--ink2);margin:0 0 8px;max-width:980px}
/* tape cells */
.tape{display:inline-grid;grid-auto-flow:column;align-items:end;gap:0;margin:2px 0}
.cellcol{display:flex;flex-direction:column;align-items:center;width:21px}
.cell{width:22px;height:22px;border:1px solid var(--cellb);margin-left:-1px;font:10px ui-monospace,monospace;display:flex;align-items:center;justify-content:center}
.cell.c1{background:var(--c1);color:#555}.cell.c0{background:var(--c0);color:#aaa}
.cell.hd{outline:3px solid var(--head);outline-offset:-1px;position:relative;z-index:1}
.hmark{height:16px;font:700 11px ui-monospace,monospace;color:var(--head);white-space:nowrap;width:21px;display:flex;justify-content:center;overflow:visible}.hmark.mk{color:var(--muted);font-weight:600}
.glrow{position:relative;height:20px;font:11.5px ui-monospace,monospace;color:var(--ink2)}
.cellcol:has(.dots){width:26px}.dots{width:26px;text-align:center;color:var(--muted);font:12px ui-monospace,monospace;align-self:center}
.glab{display:grid;grid-auto-flow:column;font:11.5px ui-monospace,monospace;color:var(--ink2)}
.gl{border-top:2px solid var(--axis);margin-top:3px;text-align:center;padding-top:1px;white-space:nowrap}
.gl.L{border-top-color:var(--s1)}.gl.w{border-top-color:var(--muted)}
.tline{display:flex;align-items:center;gap:10px;flex-wrap:wrap;margin:4px 0}
.tline .tl{min-width:118px;font-size:12.5px;color:var(--ink2)}.tline.w .tl{min-width:180px}
.dg{display:inline-flex;align-items:center;justify-content:center;min-width:19px;height:21px;padding:0 3px;border-radius:4px;font:600 12.5px ui-monospace,monospace;border:1px solid var(--line);background:var(--sunk);color:var(--ink);margin:0 1px}
.dg.L{background:var(--s1w);border-color:var(--s1)}
.dg.ch{outline:2px solid var(--s2);outline-offset:0}
.dg.end{font-weight:400;color:var(--muted);background:none;border-style:dashed}
.word{display:inline-flex;flex-wrap:wrap;align-items:center;gap:0}
.arrow{color:var(--muted);margin:0 6px}
.cl{font:650 12px ui-monospace,monospace;padding:0 5px;border-radius:4px;border:1px solid}
.cl.copied{border-color:var(--s0);background:var(--s0w)}.cl.adapted{border-color:var(--s1);background:var(--s1w)}.cl.new{border-color:var(--s2);background:var(--s2w)}
.cl.none{border-color:var(--bad);color:var(--bad)}
.mode{font:12px ui-monospace,monospace;color:var(--ink2);white-space:nowrap}
.two{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1fr);gap:16px}
.ok{color:var(--good);font-weight:700}.no{color:var(--bad);font-weight:700}
pre.cmd{background:var(--code);border-radius:6px;padding:7px 62px 7px 10px;margin:4px 0;font-size:12.5px;white-space:pre-wrap;word-break:break-all;position:relative}
button.copy{font:12px system-ui,sans-serif;border:1px solid var(--line);background:var(--surface);color:var(--ink2);border-radius:6px;padding:1px 8px;cursor:pointer;position:absolute;right:6px;top:6px}
.flow{display:flex;flex-wrap:wrap;align-items:stretch;gap:8px}
.fbox{background:var(--sunk);border:1px solid var(--line);border-radius:8px;padding:8px 10px;font-size:13px;flex:1 1 170px;max-width:290px}
.fbox b{display:block;font-size:13.5px}
.fbox.loop{border-color:var(--s1);background:var(--s1w)}
.farr{align-self:center;color:var(--muted);font-size:18px}
.bar{display:flex;height:26px;border-radius:6px;overflow:hidden;gap:2px;background:var(--surface);margin:6px 0}
.bar>div{display:flex;align-items:center;justify-content:center;font-size:12px;color:var(--ink);white-space:nowrap;overflow:hidden}
.bar .copied{background:var(--s0w);border:1px solid var(--s0)}.bar .adapted{background:var(--s1w);border:1px solid var(--s1)}
.bar .new{background:var(--s2w);border:1px solid var(--s2)}.bar .glue{background:var(--sunk);border:1px solid var(--line)}
.legend{display:flex;flex-wrap:wrap;gap:4px 14px;font-size:12.5px;color:var(--ink2);margin:4px 0}
.sw{display:inline-block;width:12px;height:12px;border-radius:3px;vertical-align:-1px;margin-right:4px;border:1px solid}
svg text{font-family:system-ui,-apple-system,"Segoe UI",sans-serif}
.gantt .bg{fill:var(--surface)}.gantt .grid{stroke:var(--line);stroke-width:1}
.gantt .lab{fill:var(--ink2);font-size:12.5px}.gantt .tick{fill:var(--muted);font-size:11px}
.gantt .b1{fill:var(--s1)}.gantt .b2{fill:var(--s2)}.gantt .ok{fill:var(--good)}.gantt .dur{fill:var(--ink2);font-size:11px}
.gantt .ttl{fill:var(--ink);font-size:12.5px;font-weight:650}
.st .c1{fill:var(--c1);stroke:var(--cellb);stroke-width:.5}.st .c0{fill:var(--c0);stroke:var(--cellb);stroke-width:.5}
.st .hd{fill:none;stroke:var(--head);stroke-width:2.2}.st .lab{fill:var(--ink2);font-size:11px;font-family:ui-monospace,monospace}
.st .hl{fill:var(--head);font-size:10px;font-weight:700;font-family:ui-monospace,monospace}
.st .gl{stroke:var(--axis);stroke-width:2}.st .gt{fill:var(--ink2);font-size:11px;font-family:ui-monospace,monospace}
.imgthumb{max-width:100%;height:auto;border:1px solid var(--line);border-radius:6px;background:#000}
details.more{margin:8px 0}details.more summary{cursor:pointer;color:var(--accent);font-size:13.5px}
/* rendered markdown */
.mdbody{max-width:980px;background:var(--surface);border:1px solid var(--line);border-radius:10px;padding:8px 26px 26px}
.mdbody h1{font-size:22px;margin:18px 0 8px}.mdbody h2{font-size:19px;margin:26px 0 6px;border-bottom:1px solid var(--line);padding-bottom:3px}
.mdbody h3{font-size:16px;margin:20px 0 6px}.mdbody h1,.mdbody h2,.mdbody h3{scroll-margin-top:44px}
.mdbody a.hl{color:var(--axis);font-weight:400;font-size:.8em}
.mdbody pre.md{background:var(--code);padding:9px 12px;border-radius:6px;overflow-x:auto;font-size:12.5px;line-height:1.45}
.mdbody table.md{border-collapse:collapse;font-size:13px;margin:8px 0}
.mdbody table.md th,.mdbody table.md td{border:1px solid var(--line);padding:4px 7px;vertical-align:top;text-align:left}
.mdbody table.md th{background:var(--sunk)}
.mdbody table.md .r{text-align:right}
.mdbody li{margin:2px 0}.mdbody blockquote{margin:8px 0;padding:6px 12px;border-left:3px solid var(--accent);background:var(--accent-weak);border-radius:4px}
.toc{font-size:13px;columns:2;max-width:980px;margin:10px 0}.toc a{display:block;color:var(--ink2)}.toc .l3{padding-left:14px}
/* code view */
.vrow{display:grid;grid-template-columns:minmax(0,1fr) 330px;gap:0 14px;border-bottom:1px solid var(--line);scroll-margin-top:40px}
.vrow:target,.vrow.tgt{background:var(--accent-weak)}
pre.code{margin:0;padding:4px 0;font-size:12.5px;line-height:1.5;overflow-x:auto;background:var(--surface)}
pre.code .ln{display:inline-block;width:42px;text-align:right;padding-right:10px;color:var(--muted);user-select:none}
pre.code .ln a{color:inherit}
pre.code .row{display:block;padding-right:8px;scroll-margin-top:60px;white-space:pre}
pre.code .row.chg{background:var(--chg)}
pre.code .row:target{background:var(--accent-weak);outline:1px solid var(--accent)}
.kw{color:var(--kw);font-weight:600}.tac{color:var(--tac)}.com{color:var(--com);font-style:italic}.str{color:var(--str)}.num{color:var(--num)}.bul{color:var(--muted);font-weight:700}
aside.note{font-size:13px;padding:8px 0}
aside.note .card{position:sticky;top:44px;background:var(--sunk);border:1px solid var(--line);border-radius:8px;padding:8px 10px}
aside.note .nt{font-weight:650;font-size:13.5px}
aside.note .nl{margin-top:4px;font-size:12.5px;color:var(--ink2)}
.dl{font:12.5px ui-monospace,monospace}
.dl .a{background:rgba(44,122,75,.14)}.dl .d{background:rgba(196,55,47,.13)}.dl .h{color:var(--accent);background:var(--sunk)}
.dl .row{display:block;white-space:pre-wrap;word-break:break-all;padding:0 8px}
.dl .n{display:inline-block;width:38px;color:var(--muted);text-align:right;margin-right:6px;user-select:none}
@media (max-width:900px){.steps{grid-template-columns:1fr 1fr}.two{grid-template-columns:minmax(0,1fr)}.vrow{grid-template-columns:minmax(0,1fr)}aside.note .card{position:static}.toc{columns:1}}
@media (max-width:700px){.wrap{padding:12px 16px 50px}nav.sec{margin:0 -16px;padding:6px 16px}.steps{grid-template-columns:1fr}table.t{display:block;overflow-x:auto;max-width:100%}figure.fig{padding:10px;overflow-x:auto}pre{max-width:100%;overflow-x:auto}h1,h2,h3,p,li{overflow-wrap:anywhere}td code,td a{overflow-wrap:normal}.mdbody{padding:8px 12px 20px}.mdbody table.md{display:block;overflow-x:auto;max-width:100%}}
'''

JS_COPY = '''<script>
document.querySelectorAll('pre.cmd').forEach(function(p){var b=document.createElement('button');b.className='copy';b.type='button';
b.textContent='copy';b.onclick=function(){var t=p.getAttribute('data-cmd')||p.innerText;navigator.clipboard.writeText(t).then(function(){b.textContent='copied';setTimeout(function(){b.textContent='copy'},1200)})};p.prepend(b)});
</script>'''


def page(title, body, css_href, extra_head=''):
    return (f'<!doctype html>\n<html lang="en"><head><meta charset="utf-8">'
            f'<meta name="viewport" content="width=device-width, initial-scale=1"><title>{esc(title)}</title>'
            f'<link rel="stylesheet" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{css_href}">{extra_head}</head><body>{body}</body></html>\n')


def dg(d, ch=False, cls=''):
    if d == 'end':
        return '<span class="dg end">end</span>'
    c = 'dg' + (' L' if d == 'L' else '') + (' ch' if ch else '') + (' ' + cls if cls else '')
    return f'<span class="{c}">{esc(d)}</span>'


def word(w, before=None):
    """Digit chips; with before, outline digits that differ."""
    out = []
    for i, d in enumerate(w):
        ch = before is not None and (i >= len(before) or before[i] != d)
        out.append(dg(d, ch))
    if not w:
        out.append('<span class="dg end">[]</span>')
    return '<span class="word">' + ''.join(out) + '</span>'


def pw(w):
    """Word with a leading L-run as a power: LLLL1L1 -> L⁴ 1L1."""
    sup = str.maketrans('0123456789', '⁰¹²³⁴⁵⁶⁷⁸⁹')
    n = len(w) - len(w.lstrip('L'))
    if n >= 2:
        return f'L{str(n).translate(sup)} {w[n:]}'.strip()
    return w


def tape_cells(cells, head=None, state=None, groups=(), left_inf=True, right_inf=True, head_label=None, marks=None):
    """cells: list of (absolute index, value). groups: (first idx, last idx, label, kind). marks: {idx: text} above cells."""
    PITCH = 21                       # .cell is 22 px wide with a -1 px overlap
    cols = []
    if left_inf:
        cols.append('<div class="cellcol"><div class="hmark"></div><div class="dots">0<sup>∞</sup></div></div>')
    for (p, v) in cells:
        hm = (head_label or (state + '▸' if state else '▼')) if p == head else (marks or {}).get(p, '')
        mk = ' mk' if (marks and p in marks and p != head) else ''
        cols.append(f'<div class="cellcol"><div class="hmark{mk}">{esc(hm)}</div>'
                    f'<div class="cell c{v}{" hd" if p == head else ""}" title="cell {p}: {v}">{v}</div></div>')
    if right_inf:
        cols.append('<div class="cellcol"><div class="hmark"></div><div class="dots">0<sup>∞</sup></div></div>')
    x0 = cells[0][0]
    off = 26 if left_inf else 0
    lab = []
    for (a, b, label, kind) in groups:
        x, w = (a - x0) * PITCH + off, (b - a + 1) * PITCH
        lab.append(f'<div class="gl {kind}" style="position:absolute;left:{x + 1}px;width:{w - 3}px">{esc(label)}</div>')
    total = off + len(cells) * PITCH + (26 if right_inf else 0)
    return (f'<div style="display:inline-block;vertical-align:top"><div class="tape">{"".join(cols)}</div>'
            f'<div class="glrow" style="width:{total}px">{"".join(lab)}</div></div>')


def S_groups(r, pos):
    g = [(pos - 2, pos - 1, 'wall', 'w')]
    for i, d in enumerate(r):
        g.append((pos + 3 * i, pos + 3 * i + 2, d, 'L' if d == 'L' else ''))
    return g


def spacetime(rows, x0, x1, cell=15, top=(), bottom=(), rule_col=True):
    """SVG space-time diagram, one row per step. top/bottom: digit brackets (first, last, label) above/below."""
    lw = 96
    W = lw + (x1 - x0 + 1) * cell + 8
    ytop = 16 + (18 if top else 0)
    H = ytop + len(rows) * cell + (22 if bottom else 6)
    o = [f'<svg class="st" width="{W}" height="{H}" viewBox="0 0 {W} {H}" role="img">']
    for p in range(x0, x1 + 1):
        if p % 3 == 0:
            o.append(f'<text class="lab" x="{lw + (p - x0) * cell + cell / 2}" y="11" text-anchor="middle">{p}</text>')

    def brackets(gs, y, ty):
        for (a, b, lab) in gs:
            xa, xb = lw + (a - x0) * cell + 1, lw + (b - x0 + 1) * cell - 1
            o.append(f'<line class="gl" x1="{xa}" y1="{y}" x2="{xb}" y2="{y}"/>'
                     f'<text class="gt" x="{(xa + xb) / 2}" y="{ty}" text-anchor="middle">{esc(lab)}</text>')
    brackets(top, ytop - 3, ytop - 6)
    for i, (n, st, pos, tape, rule) in enumerate(rows):
        y = ytop + i * cell
        txt = f'{n:>3} {st}' + (f' ({rule})' if rule and rule_col else '')
        o.append(f'<text class="lab" x="2" y="{y + cell - 4}">{esc(txt)}</text>')
        for p in range(x0, x1 + 1):
            v = tape.get(p, 0)
            o.append(f'<rect class="c{v}" x="{lw + (p - x0) * cell}" y="{y}" width="{cell}" height="{cell}"/>')
        if x0 <= pos <= x1:
            o.append(f'<rect class="hd" x="{lw + (pos - x0) * cell + 1.2}" y="{y + 1.2}" width="{cell - 2.4}" height="{cell - 2.4}"/>')
    yb = ytop + len(rows) * cell + 3
    brackets(bottom, yb, yb + 13)
    o.append('</svg>')
    return ''.join(o)


def flabel(**kw):
    return '<div class="flabel">' + ''.join(f'<span><b>{esc(k.replace("_", " "))}</b>{v}</span>' for k, v in kw.items()) + '</div>'


def tagchip(t):
    lab = {'copied': 'copied from TM7', 'adapted': 'adapted', 'new': 'new'}[t]
    return f'<span class="tag {t}">{lab}</span>'


def vlink(n, prefix='review/'):
    return f'{prefix}v.html#L{n}'


def lr(r):
    return f'{r[0]}' if r[0] == r[1] else f'{r[0]}–{r[1]}'


def lnr(r):
    """'line 20' or 'lines 20–24'."""
    return ('line ' if r[0] == r[1] else 'lines ') + lr(r)


CMDPRE = 'cd ~/projects/bb6-hunt && T=1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---'


def pdt(z):
    """'2026-10-10T17:42:06Z' -> '10:42 PDT' (UTC-7 on this date)."""
    h, m = int(z[11:13]), int(z[14:16])
    return f'{(h - 7) % 24:02d}:{m:02d} PDT'


def cmd(s):
    return f'<pre class="cmd" data-cmd="{esc(s)}">{esc(s)}</pre>'


# ============================================================== 10. sub-pages
OUT.mkdir(exist_ok=True)
(OUT / 'review.css').write_text(CSS.strip() + '\n', encoding='utf-8')

SUBNAV = ('<nav class="sec"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review.html">← #2 review</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/proof.html">proof.md</a>'
          '<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/v.html">the .v</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/diff.html">diff vs TM7</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/tm7.html">TM7 (SOMDCv6.v)</a>'
          '<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/index.html#mechanism">machine page</a></nav>')


def md_page(fname, src_rel, title, text, intro=''):
    body, toc = md(text)
    tochtml = ''
    if sum(1 for t in toc if t[0] in (2, 3)) >= 4:
        tochtml = '<div class="toc">' + ''.join(
            f'<a class="l{l}" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#</span><span class="si">{i}">{md_inline(t)}</a>' for (l, i, t) in toc if l in (2, 3)) + '</div>'
    html_ = (f'<div class="wrap">{SUBNAV}<p class="muted" style="margin-top:12px">Rendered from '
             f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{esc(src_rel)}"><code>{esc(src_rel.replace("../", ""))}</code></a> (raw file). {intro}</p>'
             f'{tochtml}<div class="mdbody">{body}</div></div>')
    (OUT / fname).write_text(page(title, html_, 'review.css'), encoding='utf-8')
    return toc


PTOC = md_page('proof.html', '../submission/proof.md', '#2 proof.md',
               PROOF_S, 'This is the submission copy, the one you would post. The working copy '
               '<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/proof.md.html"><code>proof.md</code></a> differs only in its formal-status lines '
               '(header, §4, §5, §6, §7); the working copy still says §3.3 is informal.')
PIDS = {i for (_, i, _) in PTOC}
for need in ['s1', 's2', 's3', 's3-1', 's3-2', 's3-3', 's3-4', 's3-5', 's4', 's5', 's6', 's7', 'review-log']:
    assert need in PIDS, (need, PIDS)
md_page('notes.html', '../notes.md', '#2 notes.md', NOTES, 'The running log for #2: observation, rules, Checkpoint A, kill record.')
md_page('rocq-plan.html', '../rocq-plan.md', '#2 rocq-plan.md', PLAN, 'Formalization prep, written before the domain fix in proof.md; its 3-sweep plan (§3.5) was not used.')
md_page('rocq-log.html', '../rocq/log.md', '#2 rocq/log.md', RLOG, 'The formalizer\'s log (one round).')
md_page('readme.html', '../submission/README.md', '#2 submission README', README, 'Submission one-pager.')
md_page('discord.html', '../submission/discord.md', '#2 Discord draft', DISCORD, 'Not posted.')

# ---- v.html
VH = coq_lines(VSRC)
assert len(VH) >= NV


def code_rows(lines_html, a, b, marks=()):
    out = []
    for n in range(a, b + 1):
        cls = 'row chg' if n in marks else 'row'
        out.append(f'<span class="{cls}" id="L{n}"><span class="ln"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#L</span><span class="si">{n}">{n}</a></span>{lines_html[n - 1]}</span>')
    return '<pre class="code">' + ''.join(out) + '</pre>'


def note_card(it, here='v'):
    links = []
    if it['pref']:
        links.append(f'proof.md: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/proof.html#</span><span class="si">{it["pref"][0]}">{esc(it["pref"][1])}</a>')
    if it['src']:
        links.append(f'TM7: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/tm7.html#L</span><span class="si">{it["src"][0]}">SOMDCv6.v {lr(it["src"])}</a>')
    if it['rel']:
        (r, lab) = it['rel']
        links.append(f'related: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/tm7.html#L</span><span class="si">{r[0]}">SOMDCv6.v {lr(r)}</a> ({esc(lab)})')
    extra = ''
    if it['id'] == 'RIncs':
        extra = '<div class="nl">Shaded lines differ from TM7.</div>'
    if it['id'] in ('RIncs_spec', 'nonhalt', 'tm'):
        extra = '<div class="nl">Shaded lines differ from TM7.</div>'
    if it['id'] == 'key':
        extra = (f'<div class="nl">Repeated text (a reviewer may ask to factor it): the h1_d0_0 and h1_d0_1 cases '
                 f'are identical ({FACT["dup_d0"]} lines each); rh_0, rh_1, rh_2 are identical ({FACT["dup_rh"]} each); '
                 f'hx_d1 and hx_d0 differ in one line.</div>')
    return (f'<div class="card"><div class="nt">{esc(it["title"])}</div><div>{tagchip(it["tag"])} '
            f'<span class="muted">{lnr(it["vr"])}</span></div><div class="nl" style="color:var(--ink)">{esc(it["note"])}</div>'
            + ''.join(f'<div class="nl">{x}</div>' for x in links) + extra + '</div>')


rows = []
n = 1
items_by_start = {it['vr'][0]: it for it in ITEMS}
while n <= NV:
    if n in items_by_start:
        it = items_by_start[n]
        rows.append(f'<div class="vrow" id="{esc(it["id"])}">{code_rows(VH, it["vr"][0], it["vr"][1], CHANGED)}'
                    f'<aside class="note">{note_card(it)}</aside></div>')
        n = it['vr'][1] + 1
    else:
        m2 = n
        while m2 + 1 <= NV and (m2 + 1) not in items_by_start:
            m2 += 1
        rows.append(f'<div class="vrow">{code_rows(VH, n, m2)}<aside class="note"></aside></div>')
        n = m2 + 1
vbody = (f'<div class="wrap">{SUBNAV}<h2 class="sh" style="margin-top:14px">{esc(TM)}.v</h2>'
         f'<p class="lead">The kill file, {NV} lines, sha256 <code>{V_SHA[:16]}…</code> (same file as '
         f'<code>submission/</code>). Right column: one note per item, with its tag, the proof.md section it formalizes '
         f'and TM7\'s counterpart in <code>SOMDCv6.v</code>. Tags are computed: <b>copied</b> = same text as TM7, '
         f'<b>adapted</b> = TM7\'s text with edits (edited lines shaded), <b>new</b> = no TM7 text. '
         f'Raw file: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/</span><span class="si">{esc(TM)}.v">{esc(TM)}.v</a>.</p>'
         '<div class="legend"><span>' + tagchip('copied') + '</span><span>' + tagchip('adapted') + '</span><span>' + tagchip('new') +
         '</span><span><span class="sw" style="background:var(--chg);border-color:var(--s2)"></span>line differs from TM7 (inside an adapted item)</span></div>'
         + ''.join(rows) + '</div>')
(OUT / 'v.html').write_text(page(f'#2 {TM}.v', vbody, 'review.css'), encoding='utf-8')

# ---- tm7.html (header 1-17 + Module TM7), with back-links
SH = coq_lines(SOMSRC)
back = {}
for it in ITEMS:
    for r, kind in ([(it['src'], 'source')] if it['src'] else []) + ([(it['rel'][0], 'related')] if it['rel'] else []):
        back.setdefault(r, []).append((it, kind))
segs = []
pieces = [(1, 17), (TM7_LO, TM7_HI)]
for (a, b) in pieces:
    n = a
    starts = sorted(r for r in back if a <= r[0] <= b)
    while n <= b:
        hit = [r for r in starts if r[0] == n]
        if hit:
            r = max(hit, key=lambda x: x[1])
            e = max(x[1] for x in hit)
            notes = []
            for rr in hit:
                for (it, kind) in back[rr]:
                    notes.append(f'<div class="nl">→ ours: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/v.html#</span><span class="si">{esc(it["id"])}">{esc(it["title"])}</a> '
                                 f'({lnr(it["vr"])}) {tagchip(it["tag"]) if kind == "source" else "<span class=muted>related</span>"}</div>')
            # nested related ranges (e.g. bullets inside RIncs_spec) are listed on the enclosing item
            inner = [r2 for r2 in starts if r2[0] > n and r2[1] <= e]
            for r2 in inner:
                for (it, kind) in back[r2]:
                    notes.append(f'<div class="nl">{lnr(r2)} → ours: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/v.html#</span><span class="si">{esc(it["id"])}">{esc(it["title"])}</a> '
                                 f'<span class="muted">({kind})</span></div>')
                starts.remove(r2)
            segs.append(f'<div class="vrow">{code_rows(SH, n, e)}<aside class="note"><div class="card">{"".join(notes)}</div></aside></div>')
            n = e + 1
        else:
            nxt = [r[0] for r in starts if r[0] > n]
            e = min([b] + [x - 1 for x in nxt])
            segs.append(f'<div class="vrow">{code_rows(SH, n, e)}<aside class="note"></aside></div>')
            n = e + 1
    if (a, b) == (1, 17):
        segs.append(f'<div class="vrow"><pre class="code"><span class="row"><span class="ln">…</span><span class="com">'
                    f'lines 18–{TM7_LO - 1}: Modules TM1–TM6 (not shown)</span></span></pre><aside class="note"></aside></div>')
tbody = (f'<div class="wrap">{SUBNAV}<h2 class="sh" style="margin-top:14px">TM7 in vendor/busycoq/verify/SOMDCv6.v</h2>'
         f'<p class="lead">The template, with its real line numbers: the shared header (lines 1–17) and '
         f'<code>Module TM7</code> (lines {TM7_LO}–{TM7_HI}, {TM7_HI - TM7_LO + 1} lines). TM8 (line {TM8_LO}) reuses the same proof text. '
         f'Right column: where each piece went in our file. Raw: <a href="/busy-beaver/unavailable.html">SOMDCv6.v</a>.</p>'
         + ''.join(segs) + '</div>')
(OUT / 'tm7.html').write_text(page('TM7 (SOMDCv6.v)', tbody, 'review.css'), encoding='utf-8')

# ---- diff.html
A = rd(TM7TOP).split('\n')[:-1]
B = VL
# GNU diff, i.e. exactly the command shown on the pages (difflib groups lines differently: 10 hunks, +419/-83)
gd = subprocess.run(['diff', '-u', str(TM7TOP), str(VFILE)], capture_output=True, text=True)
assert gd.returncode == 1, gd.stderr
GDV = subprocess.run(['diff', '--version'], capture_output=True, text=True).stdout.split('\n')[0]
ud = gd.stdout.split('\n')[:-1]
assert ud[0].startswith('--- ') and ud[1].startswith('+++ ') and not any(x.startswith('\\') for x in ud)
plus = sum(1 for x in ud[2:] if x.startswith('+'))
minus = sum(1 for x in ud[2:] if x.startswith('-'))
hunks = sum(1 for x in ud[2:] if x.startswith('@@'))
assert (hunks, plus, minus) == (9, 415, 77), (hunks, plus, minus)   # +413 before the header edit (2 more header lines)
# the hunks reproduce both files
ra, rb = [], []
for x in ud[2:]:
    if x.startswith('@@'):
        continue
    if x[0] in ' -':
        ra.append(x[1:])
    if x[0] in ' +':
        rb.append(x[1:])
assert set(ra) <= set(A) and set(rb) <= set(B)
FACT.update(diff_plus=plus, diff_minus=minus, diff_hunks=hunks, diff_tool=GDV)
drows = []
la = lb = 0
for x in ud[2:]:
    if x.startswith('@@'):
        mm = re.match(r'@@ -(\d+)(?:,\d+)? \+(\d+)', x)
        la, lb = int(mm.group(1)), int(mm.group(2))
        drows.append(f'<span class="row h">{esc(x)}</span>')
    elif x.startswith('+'):
        drows.append(f'<span class="row a" id="B{lb}"><span class="n"></span><span class="n"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/v.html#L</span><span class="si">{lb}">{lb}</a></span>+{esc(x[1:])}</span>')
        lb += 1
    elif x.startswith('-'):
        drows.append(f'<span class="row d"><span class="n">{la}</span><span class="n"></span>-{esc(x[1:])}</span>')
        la += 1
    else:
        drows.append(f'<span class="row"><span class="n">{la}</span><span class="n"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/v.html#L</span><span class="si">{lb}">{lb}</a></span> {esc(x[1:])}</span>')
        la += 1
        lb += 1
dbody = (f'<div class="wrap">{SUBNAV}<h2 class="sh" style="margin-top:14px">Diff: TM7 (standalone copy) → our .v</h2>'
         f'<p class="lead">Left numbers: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/rocq-scratch/TM7_toplevel.v.html"><code>rocq-scratch/TM7_toplevel.v</code></a> '
         f'(SOMDCv6.v lines 1–17 plus {TM7_LO + 1}–{TM7_HI - 1}, i.e. TM7 without its Module lines; {len(A)} lines; it passes '
         f'check_kill with TM7\'s string). Right numbers: our file ({NV} lines, links to the annotated view). '
         f'<b>{hunks}</b> hunks, <b>+{plus}</b> / <b>−{minus}</b> lines, as printed by the command below (GNU diffutils {esc(GDV.split()[-1])}).</p>'
         + cmd(f'{CMDPRE}\ndiff -u "machines/$T/rocq-scratch/TM7_toplevel.v" "machines/$T/$T.v" | less')
         + '<div class="legend"><span><span class="sw" style="background:rgba(44,122,75,.14);border-color:var(--good)"></span>added in ours</span>'
           '<span><span class="sw" style="background:rgba(196,55,47,.13);border-color:var(--bad)"></span>TM7 only</span></div>'
         + f'<div class="mdbody dl" style="max-width:none;padding:8px 0">{"".join(drows)}</div></div>' + JS_COPY)
(OUT / 'diff.html').write_text(page('#2 diff vs TM7', dbody, 'review.css'), encoding='utf-8')

# ============================================================== 11. the main page
P = []      # main page parts
REL = ''    # review.html sits in the machine dir


def a_(href, text):
    return f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{esc(href)}">{text}</a>'


# ---- header
P.append(f'''<div class="wrap">
<header class="top"><span class="rank">#2 · kill review</span><code class="tmname">{TM}</code>
<span class="cls"><b>Bell eats counter</b> <span class="muted">(sheet Results row 1035) · template SOMDCv6.v TM7, which differs only in A1</span></span>
<nav class="links"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/index.html#mechanism">machine page</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/compare.html">compare vs TM7</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/submission/index.html">submission/</a><a href="https://bbchallenge.org/{TM}">bbchallenge ↗</a><a href="/busy-beaver/machines/dashboard/machines.html">all machines</a></nav></header>
<div class="state"><span class="gtag">✓ Killed: never halts</span>
<span><code>Lemma nonhalt: ~halts tm c0.</code> · check_kill <b>PASS</b> 17/17, {FACT["rr_assump"]} axioms ·
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/submission/check_kill.txt">check_kill.txt</a> {pdt(FACT["ck_checked"])} · <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/check_kill_rerun.txt">re-run for this page</a> {pdt(FACT["rr_checked"])} (compile {FACT["rr_compile"]} s, coqchk {FACT["rr_coqchk"]} s)</span>
<span class="muted">· not posted · no Checkpoint B notes on file</span></div>
<nav class="sec"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#A"><span class="sub">A</span> Process</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#B"><span class="sub">B</span> Artifacts</a>
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#C"><span class="sub">C</span> Proof in pictures</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#D"><span class="sub">D</span> proof.md</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#E"><span class="sub">E</span> The .v</a>
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/build.py.html#F"><span class="sub">F</span> Checklist</a><span class="muted">|</span><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/proof.html">proof.md (rendered)</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/v.html">.v (annotated)</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/diff.html">diff vs TM7</a><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/compare.html">compare vs TM7</a></nav>
<div class="steps">
<div class="step"><b><span class="n">1</span>Confirm the process</b>{a_("#A", "A · timeline")}: what ran, in what order, what each stage found.</div>
<div class="step"><b><span class="n">2</span>Glance at the artifacts</b>{a_("#B", "B · artifact table")}: every file, what it is, who reads it.</div>
<div class="step"><b><span class="n">3</span>Read deeper</b>{a_("#C", "C · pictures")} first, then {a_("#D", "D · proof.md")} and {a_("#E", "E · the .v")} with margin notes.</div>
<div class="step"><b><span class="n">4</span>Judge</b>{a_("#F", "F · checklist")}: the checks a maintainer runs, and what they may push back on.</div>
</div>
<div class="callout good"><b>Correct vs reviewable.</b> The kill rests only on the .v: it compiles against unmodified busycoq,
states <code>~halts tm c0</code> for the exact holdout string, and uses no axioms (check_kill checks all of this; see F).
The informal proof, the pictures and the simulations explain it but are not part of that guarantee.
Reviewable is a separate question: can a maintainer read the file and see why it works? Section F lists what may come up.</div>
''')

# ---- A. timeline
T = [  # (row label, start, end, kind, text)   kind: a = agent work, d = Dennis, p = PASS
    ('Observe (batch of 20)', '00:06', '01:36', 'a'),
    ('Dennis: Checkpoint A', '01:22', None, 'd'),
    ('Skeptic 1 (own simulator)', '01:38', '01:56', 'a'),
    ('Aligned pictures redone', '01:56', '02:19', 'a'),
    ('Dennis: Checkpoint A', '03:31', None, 'd'),
    ('proof.md draft', '03:33', '04:25', 'a'),
    ('Rocq prep (TM7 template)', '03:33', '04:12', 'a'),
    ('Formalization round 1', '03:55', '04:46', 'a'),
    ('Skeptic 2 (proof.md)', '04:25', '04:39', 'a'),
    ('Revise proof.md', '04:39', '04:47', 'a'),
    ('Audit', '04:46', '04:47', 'a'),
    ('Bundle submission/', '04:47', '04:51', 'a'),
    ('check_kill PASS', '04:45:36', None, 'p'),
    ('check_kill PASS', '04:46:58', None, 'p'),
    ('check_kill PASS', '04:48:20', None, 'p'),
    ('check_kill PASS', '04:51:12', None, 'p'),
]


def mins(t):
    p = [int(x) for x in t.split(':')]
    return p[0] * 60 + p[1] + (p[2] / 60 if len(p) > 2 else 0)


def gantt(lo, hi, rows, title, ppm=5.0, extra=180):
    lw = 210
    W = int(lw + (hi - lo) * ppm + extra)
    rh = 22
    H = 40 + len(rows) * rh + 8
    o = [f'<svg class="gantt" width="{W}" height="{H}" viewBox="0 0 {W} {H}" role="img" aria-label="{esc(title)}">',
         f'<text class="ttl" x="0" y="13">{esc(title)}</text>']
    t = lo - lo % 30 + (30 if lo % 30 else 0)
    while t <= hi:
        x = lw + (t - lo) * ppm
        o.append(f'<line class="grid" x1="{x}" y1="34" x2="{x}" y2="{H - 6}"/>'
                 f'<text class="tick" x="{x}" y="31" text-anchor="middle">{t // 60:02d}:{t % 60:02d}</text>')
        t += 30
    for i, (lab, items) in enumerate(rows):
        y = 40 + i * rh
        o.append(f'<text class="lab" x="0" y="{y + 14}">{esc(lab)}</text>')
        for (s, e, kind, tip) in items:
            x = lw + (mins(s) - lo) * ppm
            if kind == 'a':
                w = max(3, (mins(e) - mins(s)) * ppm)
                o.append(f'<rect class="b1" x="{x:.1f}" y="{y + 3}" width="{w:.1f}" height="14" rx="3"><title>{esc(tip)}</title></rect>')
                d = int(round(mins(e) - mins(s)))
                o.append(f'<text class="dur" x="{x + w + 4:.1f}" y="{y + 14}">{s}–{e} ({d} min)</text>')
            elif kind == 'd':
                o.append(f'<path class="b2" d="M{x:.1f},{y + 2} l7,8 l-7,8 l-7,-8 z"><title>{esc(tip)}</title></path>'
                         f'<text class="dur" x="{x + 10:.1f}" y="{y + 14}">{esc(tip)}</text>')
            else:
                o.append(f'<circle class="ok" cx="{x:.1f}" cy="{y + 10}" r="3.5"><title>{esc(s)} {esc(tip)}</title></circle>')
        if items and items[0][2] == 'p':
            o.append(f'<text class="dur" x="{lw + (mins(items[-1][0]) - lo) * ppm + 8:.1f}" y="{y + 14}">'
                     f'{" · ".join(s[:5] + " " + tip.split(" (")[0] for (s, _, _, tip) in items)}</text>')
    o.append('</svg>')
    return ''.join(o)


g1 = gantt(0, 150, [
    ('Observe (20 machines)', [('00:06', '01:36', 'a', 'bb6-pilot-observe workflow')]),
    ('Dennis', [('01:22', None, 'd', '01:22 objects: "this DOES NOT seem like the only difference"')]),
    ('Skeptic 1 (own simulator)', [('01:38', '01:56', 'a', 'verify:#2')]),
    ('Aligned pictures redone', [('01:56', '02:19', 'a', 'visual:#2')]),
], 'Part 1: observe and Checkpoint A (Oct 10, PDT)')
g2 = gantt(200, 300, [
    ('Dennis', [('03:31', None, 'd', '03:31 answers Q1–Q3 (yes)')]),
    ('proof.md draft', [('03:33', '04:25', 'a', '#2:proof.md')]),
    ('Rocq prep (TM7 template)', [('03:33', '04:12', 'a', '#2:rocq-prep')]),
    ('Formalization round 1', [('03:55', '04:46', 'a', '#2:round1')]),
    ('Skeptic 2 (proof.md)', [('04:25', '04:39', 'a', '#2:skeptic')]),
    ('Revise proof.md', [('04:39', '04:47', 'a', '#2:revise')]),
    ('Audit', [('04:46', '04:47', 'a', '#2:audit')]),
    ('Bundle submission/', [('04:47', '04:51', 'a', '#2:bundle')]),
    ('check_kill PASS', [('04:45:36', None, 'p', 'formalizer'), ('04:46:58', None, 'p', 'audit (--json)'),
                         ('04:48:20', None, 'p', 'bundle (check_kill.txt)'), ('04:51:12', None, 'p', 'orchestrator')]),
], 'Part 2: proof to kill (same scale)', extra=400)

P.append(f'''<h2 class="sh" id="A"><span class="L">A</span>Process: what we did</h2>
<p class="lead">Targeting picked #2 on Oct 9. Everything else ran overnight, between 00:06 and 04:51 on Oct 10 (PDT).
The proof stages <b>overlapped</b>: Rocq prep and formalization started while proof.md was still a draft (Fig A).</p>
<figure class="fig" id="figA"><figcaption><span class="fno">Fig A</span>When each stage ran</figcaption>
<div class="tscroll">{g1}</div><div class="tscroll" style="margin-top:6px">{g2}</div>
<div class="legend"><span><span class="sw" style="background:var(--s1);border-color:var(--s1)"></span>agent work (bar = start to end)</span>
<span><span class="sw" style="background:var(--s2);border-color:var(--s2);transform:rotate(45deg)"></span>Dennis</span>
<span><span class="sw" style="background:var(--good);border-color:var(--good);border-radius:50%"></span>check_kill PASS on the final .v</span></div>
{flabel(Times="PDT, 2026-10-10; 1 minute = 5 px in both parts; 02:30–03:20 omitted (no #2 proof work)",
        Source="workflow records in ~/.claude/projects/-home-dennis/…/workflows (agent first and last message), session messages (Dennis), check_kill timestamps (UTC 11:45:36 formalizer; 11:46:58 audit, saved as <a href='/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/check_kill_audit.json'>check_kill_audit.json</a>; 11:48:20 bundle; 11:51:12 orchestrator)")}
</figure>
''')

TL = [
    ('Targeting', 'Oct 9', 'Ranked #2 of 20 pilots: it differs only in A1 from two machines mxdys proved in SOMDCv6.v (TM7 <code>…1RB0RC…</code>, TM8 <code>…1RB0LC…</code>). Risk "medium": mxdys stopped short of these two, so A1 probably breaks his rule set.',
     'Closest template: SOMDCv6.v <code>Module TM7</code> (line 1626).',
     [('../../reports/targeting.md', 'targeting.md §4.2 row 2')]),
    ('Observe', '00:06–01:36', 'Simulated to 1e9 steps and fitted rules. The tape at each sweep boundary is <code>S(r) = 0^∞ 11 D&gt; r 0^∞</code> over digits L=110, 0=000, 1=100.',
     'Our sweep map = TM7\'s plus "+1 to the rest of the word at each L entered". Fits <b>208/208</b> sweeps; TM7\'s map alone fits 1/208. Confidence high.',
     [('observe.json', 'observe.json'), ('notes.md', 'notes.md'), ('index.html#mechanism', 'machine page (index.html)')]),
    ('Checkpoint A', '01:22 → 03:31', 'Dennis objected to the first picture pair: "it seems like ours does the \u201cwalking\u201d and TM7 does the extra bouncing/zigzagging". A skeptic re-checked with its own C simulator (all 156,622 A1 events to 1e9), then the pictures were redone as aligned pairs from the same start.',
     'Mechanism confirmed, 11 corrections. Among them: the caption "TM7 eats silently" was false, and the old pair did not "show the whole difference" (same step window, different phases). One case was missing: a <b>drain pass entering an L also fires +1</b> (115/208 sweeps; without it the map fits 95/208). Dennis then answered Q1–Q3 yes and spotted the extra 1 after the first eat.',
     [('notes.md', 'notes.md § Checkpoint A'), ('img/eat_pair.png', 'eat_pair.png'), ('img/sweep_pair.png', 'sweep_pair.png')]),
    ('Informal proof', '03:33–04:25', 'Wrote proof.md by extending TM7: Inc premise in the two L clauses, then TM7\'s domain argument.',
     'TM7\'s domain lemma <b>did not carry over</b>: the domain is not closed (170 words of ≤ 11 digits fail). Fix: two zero-pass end clauses <b>Z0/Z1</b> and a generalized domain lemma <b>RIncs_nxt\'</b> with j pending +1s. All simulation checks pass.',
     [('review/proof.html', 'proof.md'), ('check_proof.py', 'check_proof.py')]),
    ('Rocq prep', '03:33–04:12 (parallel)', 'Un-wrapped TM7 into a standalone file and swapped in our string.',
     'TM7 standalone compiles in 3.8 s and passes check_kill with TM7\'s string. With our string only the two L bullets of RIncs_spec break; the new segment facts are proved by <code>esx</code>. Also found the domain counterexample <code>LLLL10LL1L1</code>; its own fix (a 3-sweep invariant, §3.5) was not used.',
     [('review/rocq-plan.html', 'rocq-plan.md'), ('rocq-scratch/TM7_toplevel.v', 'TM7_toplevel.v'), ('rocq-scratch/probe_segments_2.v', 'probe_segments_2.v')]),
    ('Formalization', '03:55–04:46 (1 round of max 4)', 'Started from TM7 while proof.md was being written (told to re-read it as it changed).',
     'proof.md\'s §3.3 case table matched the Coq cases one to one. check_kill <b>PASS</b> at 04:45:36.',
     [('review/rocq-log.html', 'rocq/log.md'), ('review/v.html', 'the .v')]),
    ('Skeptic 2 + revise', '04:25–04:47', 'Adversarial review of proof.md as a busycoq maintainer would read it, then a revision.',
     'Sound; 5 minor gaps (wrong clause counts, understated formal status, "verbatim" claim, A1 wording, an unlisted functionality assumption). All fixed; listed in proof.md\'s Review log.',
     [('review/proof.html#review-log', 'proof.md § Review log')]),
    ('Audit + re-runs', '04:46–04:51', 'An independent agent re-ran check_kill (--json), checked the string against the 778 list and read the .v end to end; the bundle step and the orchestrator each re-ran check_kill.',
     '17/17 checks pass; string at line 301 of the 778 list; nothing suspicious. In all 4 PASS runs on sha256 <code>3b29083b…</code> (formalizer, audit, bundle, orchestrator); notes.md and the ledger each count 3 of them. '
     f'Later the same day a comment-only header edit took out the repo-local paths (code unchanged); the file is now sha256 <code>{V_SHA[:8]}…</code>, and check_kill.txt and the page re-run are fresh PASS runs on it.',
     [('notes.md', 'notes.md § Kill'), ('../../reports/overnight-ledger.md', 'overnight-ledger.md')]),
    ('Bundle', '04:47–04:51', 'Made <code>submission/</code>.',
     f'The .v (same sha256), proof.md with its status lines updated, check_kill.txt (fresh run 04:48:20), README, and a Discord draft of {FACT["discord_chars"]:,} characters counting the <code>&lt;LINK&gt;</code> placeholder ({FACT["discord_chars_nolink"]:,} without it). <b>Not posted.</b>',
     [('submission/', 'submission/'), ('review/readme.html', 'README'), ('review/discord.html', 'discord.md')]),
]
P.append('<table class="t"><thead><tr><th style="width:9%">Stage</th><th style="width:10%">When</th><th style="width:31%">What happened</th>'
         '<th style="width:36%">Key finding</th><th>Artifacts</th></tr></thead><tbody>')
for (st, when, what, find_, arts) in TL:
    P.append(f'<tr><td><b>{st}</b></td><td class="mono" style="font-size:12.5px">{when}</td><td>{what}</td><td>{find_}</td>'
             f'<td>{"<br>".join(a_(h, t) for h, t in arts)}</td></tr>')
P.append('</tbody></table>')

# ---- B. artifacts
ART = [
    ('Picked and observed', [
        ('../../reports/targeting.md', 'reports/targeting.md', 'Pilot memo; §4.2 row 2 is #2.', 'Why this machine: one transition from a proved template.', 'D'),
        ('observe.json', 'observe.json', 'Observer\'s structured record: summary, mechanism, figure labels, 40 history rows, rules.', 'Feeds the card and the explorer\'s machine list.', 'T'),
        ('notes.md', 'notes.md', 'Running log: observation, candidate rules, Checkpoint A answers, kill record.', 'The narrative of record. Rendered: ' + a_('review/notes.html', 'notes.html') + '.', 'DA'),
        ('check_rules.py', 'check_rules.py', 'Observe-stage rule checks (sweep map vs the real machine).', 'Source of 208/208 and the L-entry checks.', 'A'),
        ('index.html#mechanism', 'machine page (index.html)', 'The Checkpoint A card, Figs 1–5.', 'Shows Q1–Q3 with your answers.', 'D'),
        ('img/eat_pair.png', 'img/eat_pair.png', 'Card Fig 1: one eating pass, ours vs TM7, same start S(L⁴1L1), every step.', 'Shows the +1 passes (blue) are the only difference while eating.', 'D'),
        ('img/sweep_pair.png', 'img/sweep_pair.png', 'Card Fig 2: one full sweep each.', 'Shows the drain-enters-L case (pass 5).', 'D'),
        ('img/sweep_ours.html', 'img/sweep_ours.html · sweep_tm7.html', 'Zoomable viewers of those two sweeps.', 'Hover for step, state and cell.', 'D'),
        ('img/default_site_1e4.png', 'img/default_site_1e4.png, records_1e9.png, blaze_1e7.png', 'Card Figs 3–5: site view, records to 1e9, Blaze 1e7.', 'Context only; not used by the proof.', 'D'),
        ('img/viewer.html', 'img/viewer.html', 'bbchallenge-style viewer of the first 10,000 steps (card Fig 3).', 'Context only.', 'D'),
        ('scripts/compare_tm7.py', 'scripts/compare_tm7.py', 'Regenerates the aligned pictures and their event counts.', 'Reproducibility of Figs 1–2.', 'A'),
        ('../../tools/explorer/#preset=p2-vs-tm7', 'explorer preset p2-vs-tm7', 'Interactive: #2 and TM7 from S(L⁴1L1); dashed line = first difference.', 'Spot-check any step yourself.', 'D'),
    ]),
    ('Proof (informal)', [
        ('review/proof.html', 'proof.md → rendered', 'The informal proof (working copy: ' + a_('proof.md', 'raw') + '; submission copy: ' + a_('submission/proof.md', 'raw') + ').', 'What a maintainer reads to understand the .v. §3.3 is the new idea.', 'MD'),
        ('check_proof.py', 'check_proof.py', 'Simulation checks for every claim of proof.md, plus a partial Rocq compile (--rocq).', 'Evidence, not proof. Default run: ALL PASS in 7 s (run for this page).', 'A'),
    ]),
    ('Formal proof', [
        ('review/rocq-plan.html', 'rocq-plan.md', 'Template anatomy of TM7, what breaks, risks, size estimate.', 'Found that TM7\'s domain is not closed for #2. Its 3-sweep plan was superseded by proof.md\'s Z0/Z1 fix.', 'A'),
        ('rocq-scratch/TM7_toplevel.v', 'rocq-scratch/TM7_toplevel.v', 'TM7 un-wrapped from its Module (261 lines).', 'Base of ' + a_('review/diff.html', 'the diff') + '; passes check_kill with TM7\'s string.', 'A'),
        ('rocq-scratch/probe_segments_2.v', 'rocq-scratch/probe_segments_2.v', '8 probe lemmas for the new pass segments.', 'First proof that the +1 pass is an ordinary h visit.', 'A'),
        ('rocq-scratch/py/', 'rocq-scratch/py/*.py', 'Domain experiments: rincs, domain_facts, joint, margin, margin_cond.', 'Ruled out "safety margin" invariants.', 'A'),
        ('rocq/work.v', 'rocq/work.v · rocq/compile.sh', 'Formalizer\'s work file and compile wrapper.', 'work.v = the kill file minus its header and rule-table comments, plus one unused Ltac (nxt_inc).', 'A'),
        ('review/rocq-log.html', 'rocq/log.md', 'Formalization log: what compiled, pitfalls, the kill run.', 'Round 1 was enough.', 'A'),
        ('review/v.html', f'{TM}.v → annotated', f'<b>The kill.</b> {NV} lines, top-level <code>Lemma nonhalt: ~halts tm c0.</code> (raw: ' + a_(f'{TM}.v', '.v') + ').', 'The only artifact the kill rests on.', 'MDT'),
        ('../../atlas/rocq-notes.md', 'atlas/rocq-notes.md', 'Tactics log; sections "SOMDCv6 TM7 template (for #2)" and "Machine #2 … formalization round 1".', 'Lessons for the next variant (zero-cost representation clauses).', 'A'),
        ('../../vendor/busycoq/verify/SOMDCv6.v', 'vendor/busycoq/verify/SOMDCv6.v', f'The template: TM7 at lines {TM7_LO}–{TM7_HI} (rendered: ' + a_('review/tm7.html', 'tm7.html') + ').', 'What the maintainer will compare against.', 'M'),
        ('compare.html', 'compare.html', 'Our .v vs TM7 side by side: the three machines, similarity per item, full aligned diff, proof structure (built by ' + a_('compare/build.py', 'compare/build.py') + ').',
         'How much of TM7 we kept, item by item. Its counts use its own line matching (difflib, blank lines ignored), so they differ from the GNU diff counts on this page.', 'DM'),
    ]),
    ('Verification and packaging', [
        ('../../tools/check_kill.sh', 'tools/check_kill.sh', 'The kill gate: 17 checks (pin, string, statement, forbidden words, assumptions, coqchk, …).', 'Encodes the kill criteria in CLAUDE.md.', 'T'),
        ('../../data/holdouts/2026-10-07_778.txt', 'data/holdouts/2026-10-07_778.txt', 'The current holdout list; our string is line 301.', 'A kill counts only if the string is on it.', 'T'),
        ('submission/', 'submission/', 'What you would post: the .v (same sha256), proof.md, check_kill.txt, README.md, discord.md.', 'Self-contained package.', 'DM'),
        ('submission/check_kill.txt', 'submission/check_kill.txt', f'Full check_kill output, run {pdt(FACT["ck_checked"])}.', 'Attach or quote when posting.', 'M'),
        ('review/discord.html', 'submission/discord.md', f'Draft post, {FACT["discord_chars"]:,} characters counting the <code>&lt;LINK&gt;</code> placeholder; replace it with the .v URL.', 'The post itself.', 'D'),
        ('status.json', 'status.json', '<code>KILLED_NONHALT</code>, stage done.', 'Feeds the dashboards.', 'T'),
        ('../../reports/overnight-ledger.md', 'reports/overnight-ledger.md', 'One line per orchestrator action, with times.', 'Timeline source.', 'D'),
    ]),
]
WHO = {'D': 'Dennis', 'M': 'maintainer', 'T': 'tooling', 'A': 'agents'}
P.append(f'''<h2 class="sh" id="B"><span class="L">B</span>Artifacts</h2>
<p class="lead">Every file that matters for #2, grouped by stage. "Reader" is who it is for. The green row is the kill itself.</p>
<table class="t"><thead><tr><th>Artifact</th><th>What it is</th><th>Why it matters</th><th>Reader</th></tr></thead><tbody>''')
for grp, items in ART:
    P.append(f'<tr class="grp"><td colspan="4">{esc(grp)}</td></tr>')
    for (href, label, what, why, who) in items:
        p = (M / href.split('#')[0]).resolve() if not href.startswith('http') else None
        assert p is None or p.exists(), href
        bold = ' style="background:var(--good-weak)"' if label.startswith(TM) else ''
        P.append(f'<tr{bold}><td class="mono" style="font-size:12.5px">{a_(href, esc(label))}</td><td>{what}</td><td>{why}</td>'
                 f'<td>{"".join(f"<span class=who>{WHO[c]}</span>" for c in who)}</td></tr>')
P.append('</tbody></table>')

# ---- C. pictures
cells = [(p, S_tape(W0)[p] if p in S_tape(W0) else 0) for p in range(-2, 21)]
fig1 = tape_cells(cells, head=0, state='D', groups=S_groups(W0, 0))
leg_digits = ''.join(
    f'<span class="tline"><span class="tl">digit <b class="mono">{d}</b></span>'
    + tape_cells([(i, int(c)) for i, c in enumerate(DIGC[d])], left_inf=False, right_inf=False) + '</span>'
    for d in 'L01')
EXPL = '../../tools/explorer/#preset=p2-vs-tm7'


def pass_fig():
    g = lambda w: [(3 * i, 3 * i + 2, d) for i, d in enumerate(w)]
    return spacetime(PASS, -1, 12, top=g(X), bottom=g(inc(X)) + [(-1, -1, 'exit')])


def deriv_table(steps, title, ours=True):
    o = [f'<div><div style="font-weight:650;margin-bottom:4px">{title}</div><table class="t"><thead><tr><th>#</th><th>mode, k</th>'
         f'<th>reads</th><th>clause</th><th>writes</th><th>rest after (orange = changed by +1)</th></tr></thead><tbody>']
    for i, s in enumerate(steps):
        nm = {'X1': 'RIncs_hx_ld', 'X2': 'RIncs_hx_d0', 'X3': 'RIncs_hx_d1', 'C1': 'RIncs_h1_ld', 'C2': 'RIncs_h1_d1',
              'C3': 'RIncs_h1_d0_0', 'C4': 'RIncs_h1_d0_1', 'R0': 'RIncs_h1_rh_0', 'R1': 'RIncs_h1_rh_1',
              'R2': 'RIncs_h1_rh_2', 'Z1': 'RIncs_h1_z1', 'Z0': 'RIncs_h1_z0'}[s['cl']]
        t = CL_TAG[nm] if ours else 'copied'
        before = s['rest0'][1:] if s['rd'] != 'end' else ''
        rest = word(s['rest'], before if s['inc'] else None) if s['rest'] else '<span class="muted">—</span>'
        o.append(f'<tr><td class="r">{i + 1}</td><td class="mode">{s["tp0"]}, {s["k0"]}</td><td>{dg(s["rd"])}</td>'
                 f'<td style="white-space:nowrap"><span class="cl {t}">{s["cl"]}</span>{" +1" if s["inc"] else ""}</td><td>{dg(s["out"])}</td><td>{rest}</td></tr>')
    o.append('</tbody></table></div>')
    return ''.join(o)


CLROWS = [
    ('X1', 'RIncs_hx_ld', 'hx (eater)', 'any k', 'L', 'L', 'eater, k+1, on <b>rest + 1</b>'),
    ('X2', 'RIncs_hx_d0', 'hx (eater)', 'any k', '0', 'L', 'eater, k+1'),
    ('X3', 'RIncs_hx_d1', 'hx (eater)', 'any k', '1', 'L', 'drain, k'),
    ('C1', 'RIncs_h1_ld', 'h1 (drain)', 'k ≥ 1', 'L', 'L', 'eater, k, on <b>rest + 1</b> (restart)'),
    ('C2', 'RIncs_h1_d1', 'h1 (drain)', 'k ≥ 1', '1', 'L', 'drain, k−1 (the 1 absorbs a pass)'),
    ('C3', 'RIncs_h1_d0_0', 'h1 (drain)', 'k odd', '0', '0', 'drain, (k−1)/2'),
    ('C4', 'RIncs_h1_d0_1', 'h1 (drain)', 'k even ≥ 2', '0', '1', 'drain, (k−2)/2'),
    ('R0', 'RIncs_h1_rh_0', 'h1 (drain)', 'k = 0', 'end', '1', 'done'),
    ('R1', 'RIncs_h1_rh_1', 'h1 (drain)', 'k odd', 'end', '0', 'drain, (k−1)/2, still at the end'),
    ('R2', 'RIncs_h1_rh_2', 'h1 (drain)', 'k even ≥ 2', 'end', '1', 'drain, (k−2)/2, still at the end'),
    ('Z1', 'RIncs_h1_z1', 'h1 (drain)', 'k = 0', '1 (last)', 'L', 'done: 1 100 0^∞ = 110 0^∞'),
    ('Z0', 'RIncs_h1_z0', 'h1 (drain)', 'k = 0', '0 (last)', '1', 'done: 1 000 0^∞ = 100 0^∞'),
]
cl_html = ['<table class="t"><thead><tr><th>clause</th><th>Coq name (line)</th><th>mode</th><th>count</th><th>reads</th>'
           '<th>writes</th><th>then</th><th>vs TM7</th></tr></thead><tbody>']
for (c, nm, mode, cnt, rdg, wr, then) in CLROWS:
    t = CL_TAG[nm]
    rd_html = dg(rdg) if rdg in ('L', '0', '1', 'end') else dg(rdg[0]) + f' <span class="muted">{esc(rdg[1:])}</span>'
    vs = ('same text' if t == 'copied' else f'+ Inc premise (TM7 line {CLINE7[nm]})' if t == 'adapted' else 'not in TM7')
    cl_html.append(f'<tr><td><span class="cl {t}">{c}</span></td><td class="mono" style="font-size:12px">'
                   f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(CLINE[nm])}">{nm}</a> <span class="muted">{CLINE[nm]}</span></td><td class="mode">{mode}</td>'
                   f'<td class="mode">{cnt}</td><td>{rd_html}</td><td>{dg(wr)}</td><td>{then}</td><td>{tagchip(t)} <span class="muted" style="font-size:12px">{vs}</span></td></tr>')
cl_html.append('</tbody></table>')

# Fig 5 identities
z1a = tape_cells([(0, 1), (1, 1), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0)], groups=[(1, 3, '1', ''), (4, 6, '0', '')], left_inf=False, marks={0: 'stray'})
z1b = tape_cells([(0, 1), (1, 1), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0)], groups=[(0, 2, 'L', 'L'), (3, 5, '0', '')], left_inf=False, marks={0: ' '})
z0a = tape_cells([(0, 1), (1, 0), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0)], groups=[(1, 3, '0', ''), (4, 6, '0', '')], left_inf=False, marks={0: 'stray'})
z0b = tape_cells([(0, 1), (1, 0), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0)], groups=[(0, 2, '1', ''), (3, 5, '0', '')], left_inf=False, marks={0: ' '})
stuck = CE1_NOZ_STEPS[-1]

# Fig 6 joint walk
jw = ['<table class="t"><thead><tr><th class="r">digit</th><th>first sweep: mode, k</th><th>reads</th><th>clause</th><th>writes</th>'
      '<th class="r">j</th><th>second sweep: mode, q</th><th>reads</th><th>clause</th><th>Inv(tp,k,j,tq,q)</th></tr></thead><tbody>']
for r in JW:
    if r['end']:
        fin = ' '.join(r['fin_cls'])
        need = (f'K = k+j = {r["K"]} ≤ 2q+2 = {2 * r["q"] + 2}' if r['tq'] == 'hx' else f'K = {r["K"]} ≤ q = {r["q"]}')
        lem = 'End_x' if r['tq'] == 'hx' else 'End_1'
        jw.append(f'<tr style="background:var(--s1w)"><td class="r">end</td><td class="mode">{r["tp"]}, {r["k"]}</td><td>{dg("end")}</td>'
                  f'<td><span class="cl copied">{r["cl"]}</span></td><td class="muted">…</td><td class="r">{r["j"]}</td>'
                  f'<td class="mode">{r["tq"]}, {r["q"]}</td><td>{word(r["srest"])}</td><td colspan="2"><b>{lem}</b>: {need} '
                  f'<span class="ok">✓</span>. The second sweep finishes: {" ".join(r["fin_cls"])} → writes {word(r["fin"])}; '
                  f'the last step is <span class="cl new">Z1</span>.</td></tr>')
        continue
    t1 = 'adapted' if r['c1'] in ('X1', 'C1') else 'copied'
    t2 = 'adapted' if r['c2'] in ('X1', 'C1') else 'copied'
    jw.append(f'<tr><td class="r">{r["n"]}</td><td class="mode">{r["tp"]}, {r["k"]}</td><td>{dg(r["d1"])}</td><td><span class="cl {t1}">{r["c1"]}</span></td>'
              f'<td>{dg(r["o1"])}</td><td class="r">{r["j"]}</td><td class="mode">{r["tq"]}, {r["q"]}</td>'
              f'<td>{dg(r["d2"], r["o1"] != r["d2"])}</td><td><span class="cl {t2}">{r["c2"]}</span></td><td><span class="ok">✓</span></td></tr>')
jw.append('</tbody></table>')
jw_diff = [r for r in JW if not r['end'] and r['o1'] != r['d2']]
assert len(jw_diff) == 1 and jw_diff[0]['c1'] == 'C4' and jw_diff[0]['c2'] == 'X2'
JD = jw_diff[0]

# Fig 7 BigStep rows
b_rows = []
for (n, w, pos, tape) in BOUND:
    cells7 = [(p, tape.get(p, 0)) for p in range(-3, 17)]
    b_rows.append(f'<div class="tline"><span class="tl">step {n}: S({w or "[]"})</span>'
                  + tape_cells(cells7, head=pos, state='D', groups=S_groups(w, pos)) + '</div>')
wall_st = spacetime(WALLROWS, -3, 8, top=[(-1, -1, '1'), (0, 2, 'L'), (3, 5, '1')],
                    bottom=[(-2, -1, 'wall'), (0, 2, 'L'), (3, 5, '1')])

# Fig 8 flow
NHR = ITEM['nonhalt']['vr']
LN_MS = find(VL, r'eapply multistep_nonhalt', NHR[0], NHR[1])
LN_PC = find(VL, r'eapply progress_nonhalt_cond', NHR[0], NHR[1])
LN_WIT = find(VL, r'exists \[LD;LD;LD;D1;D1\]', NHR[0], NHR[1])
LN_BS = find(VL, r'apply BigStep, I1', NHR[0], NHR[1])
LN_DOM = find(VL, r'apply \(domain _ _ I1\)', NHR[0], NHR[1])
TMV = ROOT / 'vendor/busycoq/verify/TM.v'
TL_ = rd(TMV).split('\n')
LN_MSN = find(TL_, r'^Corollary multistep_nonhalt')
LN_PCN = find(TL_, r'^Corollary progress_nonhalt_cond')


def fb(title, body_, href=None, cls='fbox'):
    t = a_(href, esc(title)) if href else esc(title)
    return f'<div class="{cls}"><b>{t}</b>{body_}</div>'


flow = ('<div class="flow">'
        + fb('c0 (blank tape)', '<div class="muted">state A, all 0</div>')
        + '<span class="farr">→</span>'
        + fb('start', f'<div>c0 -->* S(L1) in 16 steps, by computation (<code>esx</code>), line {ITEM["start"]["vr"][0]}</div>', vlink(ITEM['start']['vr'][0]))
        + '<span class="farr">→</span>'
        + fb('P(L1)', f'<div>witness: R(hx,0,L1, LLL11), built by hand from X1 (with Inc), X2, X3, R2, R0, lines {LN_WIT}–{LN_WIT + 3}. LLL11 is the real step-91 word.</div>', vlink(LN_WIT))
        + '<span class="farr">→</span>'
        + fb('for every r with P(r)', f'<div><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(LN_BS)}">BigStep</a>: <span style="white-space:nowrap">S(r) -->+ S(r\')</span> (one or more steps)</div>'
             f'<div><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(LN_DOM)}">domain</a>: P(r\')</div><div class="muted">so the run never stops making progress</div>', None, 'fbox loop')
        + '<span class="farr">→</span>'
        + fb('~halts tm c0', f'<div><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(LN_PC)}">progress_nonhalt_cond</a> (TM.v {LN_PCN}): ~halts from S(L1);'
             f' <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(LN_MS)}">multistep_nonhalt</a> (TM.v {LN_MSN}): back to c0. Line {LN_NH}.</div>')
        + '</div>')

P.append(f'''<h2 class="sh" id="C"><span class="L">C</span>The proof in pictures</h2>
<p class="lead">Eight figures, in the order the proof uses them. Abstract figures are computed from the relation R by this page's
build script; machine figures are simulations of the real table. <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{EXPL}"><b>Open in explorer: #2 vs TM7 from S(L⁴1L1) ↗</b></a></p>

<figure class="fig" id="fig1"><figcaption><span class="fno">Fig 1</span>The boundary configuration S(r)</figcaption>
<p class="why">At every sweep boundary the tape is a wall <code>11</code>, the head in state D on the next cell, then the word r written in 3-cell digits, then blank.
Busycoq calls it <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["Sp"]["vr"][0])}"><code>S' r</code></a>.</p>
{fig1}
<div style="display:flex;gap:28px;flex-wrap:wrap;margin-top:8px">{leg_digits}</div>
{flabel(Tape="S(L⁴ 1L1) = 0^∞ 11 D&gt; 110 110 110 110 100 110 100 0^∞; constructed (the start of card Figs 1–2 and of the explorer preset); never visited from blank",
        Cells="−2 … 20, head on cell 0", Colors="white = 1, black = 0; red outline + D▸ = head in state D about to read that cell; blue bar = L digit")}
</figure>

<figure class="fig" id="fig2"><figcaption><span class="fno">Fig 2</span>The +1 pass (Inc): what A1 = 0RF adds</figcaption>
<p class="why">An h pass (enter in B, leave in C) over a word adds 1 to it: read the 0/1 digits as a little-endian binary number, skip L.
At A1 both machines write 0 and step right. TM7's next state C turns back at once (C0 = 0LC); ours goes to F (F0 = 0RB), which starts one such pass
over everything to the right and comes back to exactly where TM7 is right after its A1 step.
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["Inc"]["vr"][0])}">Inc</a> is the relation, <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["Inc_spec"]["vr"][0])}">Inc_spec</a> the machine fact.</p>
<div class="two"><div>
<div class="tline"><span class="tl">before: 1 1 L 0</span>{word("11L0")}<span class="muted mono" style="font-size:12px">= 1·1 + 1·2 + 0·4 = 3</span></div>
<div class="tline"><span class="tl">after: 0 0 L 1</span>{word("00L1", "11L0")}<span class="muted mono" style="font-size:12px">= 0·1 + 0·2 + 1·4 = 4</span></div>
<table class="t" style="margin-top:10px"><thead><tr><th>Inc clause</th><th>proof.md</th><th>reads</th><th>writes</th></tr></thead><tbody>
<tr><td class="mono"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(find(VL, r'^\| Inc_d1'))}">Inc_d1</a></td><td>I1</td><td>{dg("1")}</td><td>{dg("0")} and carry into the rest</td></tr>
<tr><td class="mono"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(find(VL, r'^\| Inc_d0'))}">Inc_d0</a></td><td>I2</td><td>{dg("0")}</td><td>{dg("1")}, stop</td></tr>
<tr><td class="mono"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(find(VL, r'^\| Inc_ld'))}">Inc_ld</a></td><td>I3</td><td>{dg("L")}</td><td>{dg("L")}, keep going</td></tr>
<tr><td class="mono"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(find(VL, r'^\| Inc_nil'))}">Inc_nil</a></td><td>I4</td><td>{dg("end")}</td><td>{dg("1")} (append)</td></tr>
</tbody></table></div>
<div class="tscroll">{pass_fig()}</div></div>
{flabel(Start="constructed: 1 B&gt; 100 100 110 000 0^∞ (the 1 on the left is arbitrary; the pass never reads it)",
        Rows=f"every step, 0 … {len(PASS) - 1} (= 6j+1 with j = 3 digits before the first 0); label = step, state, rule just fired",
        Window="cells −1 … 12, 1 cell = 15 px", Colors="white = 1, black = 0, red box = head; A1 never fires inside the pass")}
</figure>

<figure class="fig" id="fig3"><figcaption><span class="fno">Fig 3</span>The sweep relation R (busycoq <code>RIncs</code>): 12 clauses</figcaption>
<p class="why">R(mode, k, r, r') says: a sweep in this mode with k queued passes turns word r into word r'. Read a row as "in this mode, with this count, reading this digit,
the sweep writes that digit and continues as …". 8 rows are TM7's text; X1 and C1 add the +1; Z1 and Z0 are new.</p>
<div class="tscroll">{"".join(cl_html)}</div>
<details class="more"><summary>Machine-level view of X1 (card Fig 1, eat_pair.png)</summary>
<p class="why">{esc(FIG1["why"])}</p>
<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/img/eat_pair.png"><img class="imgthumb" src="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/img/eat_pair.png" alt="eat_pair" width="726" height="670"></a>
{flabel(Start=esc(FIG1["start"]), Rows=esc(FIG1["rows"]), Window=esc(FIG1_WINDOW), Colors=esc(FIG1["legend"]))}
</details>
{flabel(What="all clauses of RIncs in the .v (" + lnr(ITEM["RIncs"]["vr"]) + "), compared constructor by constructor with TM7 (" + lnr(ITEM["RIncs"]["src"]) + ")",
        Colors="grey = TM7's text, blue = TM7's clause + Inc premise, orange = new; digit chips: blue = L")}
</figure>

<figure class="fig" id="fig4"><figcaption><span class="fno">Fig 4</span>R at work: one sweep from S(L⁴ 1L1), ours vs TM7</figcaption>
<p class="why">Each row applies one clause. Ours adds +1 to the rest at every L (X1, C1). After the first eat, ours' rest is <code>1L11</code> where TM7's is <code>1L1</code>:
that is the extra 1 you spotted at Checkpoint A. The drain pass that re-enters the L adds +1 again (<code>11 → 001</code>), so ours eats two more digits.</p>
<div class="two">{deriv_table(OURS_ST, f"ours → S({pw(OURS_OUT)})")}{deriv_table(TM7_ST, f"TM7 → S({pw(TM7_OUT)})", ours=False)}</div>
{flabel(What="derivations of R(hx, 0, L⁴1L1, ·) for both relations (abstract, computed)",
        Check=f"the real machines agree: S(L⁴1L1) → S({pw(OURS_OUT)}) in 421 steps (ours) and S({pw(TM7_OUT)}) in 237 (TM7), simulated for this page; same as card Fig 2",
        Colors="clause chips as in Fig 3; orange outline = digit changed by the +1")}
</figure>

<figure class="fig" id="fig5"><figcaption><span class="fno">Fig 5</span>Why Z0 and Z1: without them the domain is not closed</figcaption>
<p class="why">TM7's proof needs: if r can be swept, so can its output. With only the +1 change this fails. Z1 and Z0 add no machine behaviour: each says two spellings of the same tape are equal.</p>
<div class="two"><div>
<div class="tline w"><span class="tl">Z1: stray 1, then digit 1</span>{z1a}</div>
<div class="tline w"><span class="tl">= digit L</span>{z1b}</div>
<div class="tline w" style="margin-top:8px"><span class="tl">Z0: stray 1, then digit 0</span>{z0a}</div>
<div class="tline w"><span class="tl">= digit 1</span>{z0b}</div></div>
<div>
<div class="tline"><span class="tl">r</span>{word(CE0)}</div>
<div class="tline"><span class="tl">sweep(r)</span>{word(CE1)}</div>
<div class="tline"><span class="tl">without Z0/Z1</span><span class="cl none">stuck</span><span class="ink2" style="font-size:13px">drain with {stuck["k"]} passes left at the last digit <b class="mono">{stuck["rest"]}</b>: no clause</span></div>
<div class="tline"><span class="tl">with Z1</span>{word(CE2)}</div>
<p class="why" style="margin-top:8px">The real machine agrees: S(r) → S(sweep r) in {fmt(FACT["ce_steps"][0])} steps, then → S({pw(CE2)}) in {fmt(FACT["ce_steps"][1])} steps (simulated for this page).
Over all words of ≤ 11 digits: without Z0/Z1, {fmt(FACT["dom_noz"])} words can be swept and <b>{FACT["fail_noz"]}</b> of them have an output that cannot; with Z0/Z1, {fmt(FACT["dom_z"])} words can be swept and every output can be swept again (recomputed here; proof.md §3.3).
Z0/Z1 were never used in the first 3,000 sweeps from blank (simulation, not proof; proof.md §7).</p></div></div>
{flabel(Left="cells of the two identities (z1_eq line " + str(ITEM["z1_eq"]["vr"][0]) + ", z0_eq line " + str(ITEM["z0_eq"]["vr"][0]) + ")",
        Right="the counterexample from rocq-plan.md §3.5 and proof.md §3.3", Colors="cells: white = 1, black = 0; chips: blue = L")}
</figure>

<figure class="fig" id="fig6"><figcaption><span class="fno">Fig 6</span>The domain lemma <code>key</code>, run on that example</figcaption>
<p class="why"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["key"]["vr"][0])}">key</a> follows two sweeps at once: the first over r (count k), the second over the first's output (count q), one digit per row.
The second sweep's +1s land on the first's output. Lemma A (<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["RIncs_Inc"]["vr"][0])}">RIncs_Inc</a>) says that is the same as the first sweep run with
<b>j</b> extra passes, so the pair is tracked by numbers alone. <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["Inv"]["vr"][0])}">Inv</a> says q is large enough; it holds on every row.
Row {JD["n"]} shows the j +1s at work: the first writes {dg(JD["o1"])} but the second reads {dg(JD["d2"], True)}, because K = k+j = {JD["K"]} is odd.
At the end, <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["End_x"]["vr"][0])}">End_x</a> finishes the second sweep, and its last step needs Z1.</p>
<div class="tscroll">{"".join(jw)}</div>
{flabel(What=f"key's induction (one row per case, as in the Coq proof) on r = {CE0}; first sweep R(hx,0,r,·), second R(hx,0,sweep r,·)",
        Check="every row asserts Inv and that R(tp, k+j, rest) equals what the second sweep reads (Lemma A)", Colors="clause chips as in Fig 3; orange outline (second sweep's reads column) = digit the pending +1s changed, so it differs from what the first sweep wrote")}
</figure>

<figure class="fig" id="fig7"><figcaption><span class="fno">Fig 7</span>BigStep on the real machine: each sweep ends one cell further left</figcaption>
<p class="why"><a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{vlink(ITEM["BigStep"]["vr"][0])}">BigStep</a> (TM7's text): if R(hx,0,r,r') then S(r) -->+ S(r'). The pass h' turns <code>1 D&gt; r</code> into <code>&lt;C r'</code>,
then 3 steps (C1, D0, D0) rebuild the wall one cell to the left.</p>
<div>{"".join(b_rows)}</div>
<div style="margin-top:8px"><div class="muted" style="font-size:12.5px">The wall rule at the end of the first sweep, steps 13–16:</div><div class="tscroll">{wall_st}</div></div>
{flabel(Start="blank tape", Rows="steps 5, 16, 91 (the first three sweep boundaries); below: steps 13–16, every step",
        Window="cells −3 … 16 (top), −3 … 8 (bottom)", Colors="white = 1, black = 0, red = head; bars: grey = wall 11, blue = L digit")}
</figure>

<figure class="fig" id="fig8"><figcaption><span class="fno">Fig 8</span>How <code>nonhalt</code> is assembled ({lnr(NHR)})</figcaption>
{flow}
{flabel(Lemmas="framework: multistep_nonhalt and progress_nonhalt_cond in vendor/busycoq/verify/TM.v; ours: start, BigStep, domain",
        Difference_from_TM7="TM7 starts at S(1) (step 5), builds the witness with <code>repeat ec</code> and calls RIncs_nxt inline")}
</figure>
''')

# ---- D. proof.md map
DMAP = [
    ('s1', 'Families and notation', 'Digits, +1, S(r), the passes h and h\', R.', ['digits', 'passes', 'RDH', 'toRC', 'Sp', 'Inc']),
    ('s2', 'Rule table', 'Inc (I1–I4), R\'s 12 clauses, the machine-level pass rules, the worked example (Fig 4).', ['Inc', 'RIncs', 'table']),
    ('s3-1', 'Every clause is an exact run', 'Soundness of each clause; the new X1/C1 segments; Z0/Z1 as identities.', ['z1_eq', 'z0_eq', 'Inc_spec', 'seg_hx_ld', 'seg_h1_ld', 'RIncs_spec']),
    ('s3-2', 'Sweep', 'S(r) -->+ S(r\') (Fig 7).', ['BigStep']),
    ('s3-3', 'The domain is closed', 'Why Z0/Z1 are needed (Fig 5); Lemma A, Total_1, End_1, End_x; the key lemma and its case table (Fig 6).',
     ['Inc_total', 'Inc_fun', 'RIncs_Inc', 'RIncs_nxt_1', 'End_1', 'End_x', 'inv', 'Inv', 'key', 'domain']),
    ('s3-4', 'Progress', 'Each sweep is at least 4 steps.', []),
    ('s3-5', 'The halting transition F1', 'Never reached, since every rule is an exact run.', []),
    ('s4', 'Initial segment', 'Blank → S(1) in 5 steps (the .v starts at S(L1), step 16).', ['start']),
    ('s5', 'Conclusion', 'multistep_nonhalt + progress_nonhalt_cond (Fig 8).', ['nonhalt', 'domain']),
    ('s6', 'Mapping to SOMDCv6 TM7', 'Item-by-item comparison; section E below is the computed version.', []),
    ('s7', 'Evidence', 'Simulation tables (check_proof.py). Not part of the kill.', []),
    ('review-log', 'Review log', 'The skeptic\'s 5 minor gaps and their fixes.', []),
]
P.append(f'''<h2 class="sh" id="D"><span class="L">D</span>proof.md, rendered</h2>
<p class="lead">Read it here: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/proof.html"><b>review/proof.html</b></a> (the submission copy). Map of its sections to the .v:</p>
<table class="t"><thead><tr><th>§</th><th>title</th><th>what it says</th><th>formalized by</th></tr></thead><tbody>''')
for (sid, title, what, items) in DMAP:
    num = sid[1:].replace('-', '.') if sid.startswith('s') else '—'
    il = ', '.join(f'<a class="mono" style="font-size:12.5px" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/v.html#</span><span class="si">{esc(i)}">{esc(ITEM[i]["title"].split(" (")[0].replace("Lemma ", "").replace("Definition ", "").replace("Inductive ", "").replace("Notation ", "").replace("Fixpoint ", ""))}</a>' for i in items) or '<span class="muted">(no lemma: follows from the others)</span>' if sid in ('s3-4', 's3-5') else ', '.join(f'<a class="mono" style="font-size:12.5px" href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/v.html#</span><span class="si">{esc(i)}">{esc(ITEM[i]["title"].split(" (")[0].replace("Lemma ", "").replace("Definition ", "").replace("Inductive ", "").replace("Notation ", "").replace("Fixpoint ", ""))}</a>' for i in items) or '<span class="muted">—</span>'
    P.append(f'<tr><td class="mono">{a_("review/proof.html#" + sid, num)}</td><td>{esc(title)}</td><td>{what}</td><td>{il}</td></tr>')
P.append('</tbody></table>')
P.append('<div class="callout warn">Two copies exist. <b>submission/proof.md</b> (rendered above) says "fully formalized". '
         'The working <b>proof.md</b> still says §3.3 and nonhalt are informal; only its status lines are stale. '
         'One wording trap in both: in §5 and §6, "I1 passed twice" means the Coq hypothesis named <code>I1</code>, not Inc clause I1.</div>')

# ---- E. the .v
tot = NV
barp = ''.join(f'<div class="{t}" style="width:{TAGLINES[t] / tot * 100:.2f}%" title="{t}: {TAGLINES[t]} lines">{t if t != "glue" else "other"} {TAGLINES[t]}</div>'
               for t in ('copied', 'adapted', 'new', 'glue'))
idx = ['<table class="t"><thead><tr><th>lines</th><th>item</th><th>tag</th><th>in plain English</th><th>proof.md</th><th>TM7 (SOMDCv6.v)</th></tr></thead><tbody>']
for it in ITEMS:
    tm7c = (f'<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/tm7.html#L</span><span class="si">{it["src"][0]}">{lr(it["src"])}</a>' if it['src'] else
            (f'<span class="muted">related:</span> <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/tm7.html#L</span><span class="si">{it["rel"][0][0]}">{lr(it["rel"][0])}</a>' if it['rel'] else '<span class="muted">—</span>'))
    pr = a_('review/proof.html#' + it['pref'][0], esc(it['pref'][1])) if it['pref'] else '<span class="muted">—</span>'
    idx.append(f'<tr><td class="mono" style="font-size:12.5px;white-space:nowrap">{a_("review/v.html#" + it["id"], lr(it["vr"]))}</td>'
               f'<td class="mono" style="font-size:12.5px">{esc(it["title"])}</td><td>{tagchip(it["tag"])}</td><td>{esc(it["note"])}</td>'
               f'<td style="white-space:nowrap">{pr}</td><td style="white-space:nowrap">{tm7c}</td></tr>')
idx.append('</tbody></table>')
P.append(f'''<h2 class="sh" id="E"><span class="L">E</span>The .v, annotated</h2>
<p class="lead">Read it here: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/v.html"><b>review/v.html</b></a>: line numbers, highlighting, a margin note per item, lines that differ from TM7 shaded.
Also: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/diff.html">diff vs TM7</a> ({FACT["diff_hunks"]} hunks, +{FACT["diff_plus"]} / −{FACT["diff_minus"]} by GNU <code>diff -u</code>) and <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/tm7.html">TM7 with its own line numbers</a>.</p>
<figure class="fig" id="figE"><figcaption><span class="fno">Fig E</span>Where the {NV} lines come from</figcaption>
<div class="bar">{barp}</div>
<div class="legend"><span>{tagchip("copied")} same text as TM7 ({TAGCOUNT["copied"]} items)</span><span>{tagchip("adapted")} TM7's text with edits ({TAGCOUNT["adapted"]} items)</span>
<span>{tagchip("new")} no TM7 text ({TAGCOUNT["new"]} items)</span>
<span><span class="sw" style="background:var(--sunk);border-color:var(--line)"></span>other: {GLUE_KIND["blank"]} blank, {GLUE_KIND["scope"]} Scope, {GLUE_KIND["section"]} section-comment line{"s" if GLUE_KIND["section"] != 1 else ""}</span></div>
<p class="why" style="margin-top:6px">Of the {TAGLINES["adapted"]} adapted lines, {len(CHANGED)} differ from TM7 (shaded in <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/v.html">v.html</a>); the rest are TM7's text.
So about {TAGLINES["copied"] + TAGLINES["adapted"] - len(CHANGED)} of the {NV} lines are TM7's text (not counting the {TAGLINES["glue"]} other lines). Of the {TAGLINES["new"]} new lines, {NEW33} belong to the domain proof (proof.md §3.3);
<code>key</code> alone is {FACT["key_len"]}.</p>
{flabel(What=f"lines of {TM}.v by item tag; TM7 itself is {FACT['tm7_len']} lines (SOMDCv6.v {TM7_LO}–{TM7_HI})",
        Tags="computed by comparing each item's text with its TM7 source; an item with no TM7 source is new")}
</figure>
<div class="tscroll">{"".join(idx)}</div>
''')

# ---- F. checklist
CHK = [
    ('It compiles against unmodified busycoq, states the right theorem, and uses no axioms',
     'check_kill: pinned busycoq (0940bb9c), byte-exact string, top-level <code>nonhalt : ~halts tm c0</code> with absolute names, no forbidden words, '
     '<code>Print Assumptions</code> within the baseline, coqchk.',
     'tools/check_kill.sh "machines/$T/$T.v" "$T"',
     f'<code>RESULT: PASS -- this is a kill</code>, 17 <code>[PASS]</code> lines. Today ({pdt(FACT["rr_checked"])}): PASS, compile {FACT["rr_compile"]} s, coqchk {FACT["rr_coqchk"]} s, {RRWALL:.1f} s wall in all (<a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/check_kill_rerun.txt">output</a>).'),
    ('The string is a current holdout',
     'Maintainers check the machine is still open.',
     'grep -nx "$T" data/holdouts/2026-10-07_778.txt',
     f'<code>301:{TM}</code> (the list has 778 lines). Also search #bb6 and the sheet for a claim before posting (targeting code A).'),
    ('The theorem statement',
     'The two lines a maintainer reads first.',
     f'sed -n \'{LN_TM}p;{LN_NH}p\' "machines/$T/$T.v"',
     f'line {LN_TM}: <code>Definition tm := Eval compute in (TM_from_str "{TM}").</code><br>line {LN_NH}: <code>Lemma nonhalt: ~halts tm c0.</code>'),
    ('The file you post is the file that passed',
     'Same bytes in machines/ and submission/.',
     'sha256sum "machines/$T/$T.v" "machines/$T/submission/$T.v"',
     f'both <code>{V_SHA[:16]}…</code> (matches check_kill.txt).'),
    ('What changed vs TM7',
     'A maintainer compares with the template (mxdys\'s SOMDCv6.v).',
     'diff -u "machines/$T/rocq-scratch/TM7_toplevel.v" "machines/$T/$T.v" | less',
     f'{FACT["diff_hunks"]} hunks, +{FACT["diff_plus"]} / −{FACT["diff_minus"]} lines (this command, GNU diff); same thing rendered: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/diff.html">diff.html</a>. Section E tags every item.'),
    ('Spot-check the one rule change on the real machine',
     'That A1 = 0RF really is "one +1 pass, then where TM7 is".',
     'python3 -B "machines/$T/check_rules.py" --lentry',
     f'CLI: L entry ours/TM7, eater/drain, 1393/1393 each (0.5 s, run for this page). Visually: <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/</span><span class="si">{EXPL}">explorer preset ↗</a>, '
     'the two runs agree until the dashed line (A1); press d for the diff view.'),
    ('The informal claims hold on samples (optional)',
     'Evidence only; not needed for the kill.',
     'python3 -B "machines/$T/check_proof.py"',
     'ALL PASS in about 7 s (run for this page). <code>--full</code> takes longer and adds the Rocq partial check.'),
]
P.append('<h2 class="sh" id="F"><span class="L">F</span>Reviewer checklist</h2>'
         '<p class="lead">What a busycoq maintainer checks, and how you can check it yourself. Run this once in a WSL shell, then each command below:</p>'
         + cmd(CMDPRE) +
         '<table class="t" style="margin-top:10px"><thead><tr><th style="width:17%">check</th><th style="width:17%">why</th><th style="width:35%">command</th>'
         '<th>expected (and today\'s result)</th></tr></thead><tbody>')
for (c, why, cm, exp) in CHK:
    P.append(f'<tr><td><b>{c}</b></td><td>{why}</td><td>{cmd(cm)}</td><td>{exp}</td></tr>')
P.append('</tbody></table>')

# submission/proof.md: lines a maintainer would trip on if it is posted with the .v (all located, not hand-entered)
PSL = PROOF_S.split('\n')
PS = dict(note=find(PSL, r'^> Submission copy of the working'), dennis=find(PSL, r'the extra 1 Dennis noticed'),
          cp1=find(PSL, r'^This section compiles\. `check_proof\.py --rocq`'), cp2=find(PSL, r'^The checks are in `check_proof\.py`, in this directory'),
          z1=find(PSL, r'sideRLseq_O` \(via `applys_eq`\)'), z2=find(PSL, r'Z0/Z1 by `sideRLseq_O` and `const_unfold`'),
          never=find(PSL, r'^Z0/Z1 are never used on the run from blank'),
          s4L1=find(PSL, r'^The \.v file starts one sweep later'), s5=find(PSL, r"^Use `multistep_nonhalt` with `c' = S\(1\)`"),
          s5L1=find(PSL, r"^In the \.v file `c' = S\(L1\)`"), a1=find(PSL, r'exactly where TM7 is one step after its A1'),
          rlog=find(PSL, r'^## Review log$'))
PS['rlog_end'] = max(n for n in range(1, len(PSL) + 1) if PSL[n - 1].strip())
assert not (M / 'submission/check_proof.py').exists() and 'sideRLseq_O' not in '\n'.join(VL)
assert 'RSpec2.v' in '\n'.join(PSL[PS['rlog'] - 1:]) and 'notes.md' in '\n'.join(PSL[PS['rlog'] - 1:])
LN_ZEQ = find(VL, r'rewrite z1_eq\. constructor\.')
assert VL[LN_ZEQ].strip() == '- cbn[lpow app]. rewrite z0_eq. constructor.'
assert 'exactly where TM7 is one step after its A1' in DISCORD
FACT['proofmd_lines'] = PS
assert not re.search(r'(?<![\w.-])(?:vendor|machines|tools|rocq|scripts|reports)/', '\n'.join(VL[:ITEM['hdr']['vr'][1]]))

RV = [
    ('fine', 'Header comment cites no repo paths',
     f'Lines 1–{ITEM["hdr"]["vr"][1]} name 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 as busycoq commit, Coq version and the <code>Print Assumptions</code> result. Until the 2026-10-10 comment-only edit they named '
     '<code>vendor/busycoq/verify/SOMDCv6.v</code>, <code>machines/…/proof.md</code> and <code>tools/check_kill.sh</code>.',
     'None.', a_(vlink(1), f'lines 1–{ITEM["hdr"]["vr"][1]}')),
    ('likely', 'proof.md has internal and stale lines',
     f'Only matters if you post <code>submission/proof.md</code> with the .v (the README lists it). '
     f'Line {PS["note"]}: the "Submission copy…" note. Line {PS["dennis"]}: "the extra 1 Dennis noticed" at "the Checkpoint A picture pair". '
     f'Lines {PS["cp1"]} and {PS["cp2"]} cite <code>check_proof.py</code> ("in this directory"), which is not in <code>submission/</code>. '
     f'§5 line {PS["s5"]} uses <code>c\' = S(1)</code> while the .v starts at S(L1); only line {PS["s5L1"]} corrects it. '
     f'Line {PS["never"]} says Z0/Z1 "are never used on the run from blank", which is simulation evidence (3,000 sweeps). '
     f'Lines {PS["z1"]} and {PS["z2"]} prove Z0/Z1 by <code>sideRLseq_O</code> (line {PS["z1"]}: "via <code>applys_eq</code>"); the .v uses <code>rewrite z1_eq. constructor.</code> ({lnr((LN_ZEQ, LN_ZEQ + 1))}). '
     f'The Review log (lines {PS["rlog"]}–{PS["rlog_end"]}) describes our skeptic process, <code>RSpec2.v</code> and notes.md.',
     f'Drop line {PS["note"]}, the Dennis aside and the Review log; drop the check_proof.py references or ship the script; say "not used in the first 3,000 sweeps"; '
     f'describe Z0/Z1 as the .v does; for §5 see "start" below. Optional: "one step after its A1" (line {PS["a1"]}, also the Discord draft) reads better as "right after its A1 step".',
     a_('review/proof.html', 'proof.md')),
    ('maybe', f'Length: {NV} lines vs TM7\'s {FACT["tm7_len"]} (2.4×)',
     f'<code>key</code> alone is {FACT["key_len"]} lines. Repeated text inside it: h1_d0_0 = h1_d0_1 ({FACT["dup_d0"]} lines each), rh_0 = rh_1 = rh_2 ({FACT["dup_rh"]} each), '
     f'hx_d1 and hx_d0 differ in one line ({FACT["dup_hx"]} each). TM7 compresses its case analysis with <code>solve_v1</code>/<code>solve_v2</code>.',
     'Optional: merge the identical bullets (e.g. <code>1-2:</code> goal selectors or a local Ltac). Not tried.', a_('review/v.html#key', 'key')),
    ('maybe', 'The start differs from TM7 without need',
     f'<code>start</code> goes to S(L1) and the witness for P is built by hand (lines {ITEM["start"]["vr"][0]}–{LN_WIT + 3}). '
     'rocq-plan.md §3.5 picked S(L1) for an invariant that also required r to be a sweep output; the final invariant does not. '
     'TM7\'s text (<code>S\' [D1]</code>, <code>1: esx.</code>, <code>2: repeat ec.</code>) also works here: I compiled that variant in a scratch copy today (4.0 s, Print Assumptions closed; not run through check_kill).',
     f'Use TM7\'s lines; then nonhalt differs from TM7 only in the domain call, and proof.md §4/§5 (which use S(1)) are correct as written, so the S(L1) notes (lines {PS["s4L1"]} and {PS["s5L1"]}) can go.', a_('review/v.html#nonhalt', 'nonhalt')),
    ('maybe', 'Generic names', '<code>key</code>, <code>domain</code>, <code>start</code>. proof.md calls key <code>RIncs_nxt\'</code>; TM7\'s is <code>RIncs_nxt</code>.',
     'Rename key to RIncs_nxt\' so the parallel with TM7 is visible.', a_('review/v.html#key', 'key')),
    ('fine', 'Rule-table comment at the end', 'Same fenced comment block that upstream files end with (e.g. <code>1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v</code>).', 'None.', a_('review/v.html#table', 'table')),
    ('fine', 'Imports and helpers', 'Exactly SOMDCv6.v\'s header; check_kill\'s allowlist accepts them. Copied items are byte-identical to TM7 (computed in E).', 'None.', a_('#E', 'E')),
    ('local', 'Stale lines in our own notes', f'Working proof.md says "partly formal"; notes.md still has "Informal proof: Not started" and empty "Formalization log"/"Outcome" sections. '
     f'notes.md § Kill ("1,371 characters plus <code>&lt;LINK&gt;</code>") and the discord.md header ("1,371 characters before the link") both count the placeholder already ({FACT["discord_chars_nolink"]:,} without it). Not in the post.', 'Housekeeping only.', a_('review/notes.html', 'notes')),
]
P.append('<h3>Reviewability: what a maintainer may push back on</h3><p class="lead">My read of the .v and of <code>submission/proof.md</code>, as a maintainer might read them; "how likely" is my guess. None of these affect correctness, and none are applied.</p>'
         '<table class="t"><thead><tr><th style="width:8%">how likely</th><th style="width:17%">issue</th><th>details</th><th style="width:24%">possible fix</th><th style="width:7%">where</th></tr></thead><tbody>')
LK = {'likely': ('var(--caution)', 'likely'), 'maybe': ('var(--accent)', 'maybe'), 'fine': ('var(--good)', 'fine as is'), 'local': ('var(--muted)', 'local only')}
for (lk, issue, det, fix, where) in RV:
    col, lab = LK[lk]
    P.append(f'<tr><td><span class="chip" style="border-color:{col}">{lab}</span></td><td><b>{issue}</b></td><td>{det}</td><td>{fix}</td><td>{where}</td></tr>')
P.append('</tbody></table>')
P.append(f'''<h3>Before posting</h3>
<ul>
<li>Run the first four checks above (about a minute).</li>
<li>Search #bb6 and the sheet for the string (targeting code A). Targeting also suggested asking mxdys whether SOMDCv6 was tried on this machine (code B); with a proof in hand that is optional.</li>
<li>Your read of proof.md is effectively Checkpoint B. If you have notes, fold them into both proof.md copies (notes.md § Kill says so too). If you post proof.md, fix its "likely" row above first.</li>
<li>Fill <code>&lt;LINK&gt;</code> in the <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/discord.html">Discord draft</a> ({FACT["discord_chars"]:,} characters with the placeholder; Discord's limit is 2,000).</li>
<li>If you take any fix from the table above, re-run check_kill on the edited file and copy it into <code>submission/</code> again (the sha256 will change).</li>
</ul>
<p class="muted" style="margin-top:22px;font-size:12.5px">Built by <a href="/busy-beaver/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/review/review/build.py.html">review/build.py</a> from the files above; every line number, count and derivation on this page is computed and asserted there.
Stage times come from the workflow records and are hand-entered.</p>
</div>{JS_COPY}''')

(M / 'review.html').write_text(page('#2 kill review', ''.join(P), 'review/review.css'), encoding='utf-8')
print(json.dumps({k: v for k, v in FACT.items()}, indent=0))
print('tags', TAGCOUNT, TAGLINES, 'changed lines', len(CHANGED))
print('wrote', M / 'review.html', 'and', sorted(p.name for p in OUT.iterdir()))