#!/usr/bin/env bash
# tools/check_kill.sh -- the BB(6) kill oracle (PLAN.md section 3, ground rule 1).
#
# usage: tools/check_kill.sh [options] <file.v> <tm>
#
# A kill counts only if this script prints RESULT: PASS and exits 0. That needs ALL of:
#   (a) vendor/busycoq HEAD == tools/busycoq.pin, no tracked changes under verify/,
#       and every framework .vo the file needs exists and is newer than its .v (with the
#       native compiler on, also its .coq-native code, no older than the .vo);
#   (b) the TM_from_str literal in the file's top-level `Definition tm` equals <tm>
#       byte for byte (text), AND Rocq accepts `tm = TM_from_str "<tm>"` by eq_refl,
#       stated with fully qualified framework names;
#   (c) Rocq accepts `nonhalt : ~ halts (TM_from_str "<tm>") c0` (or, with --halt,
#       `halt : halts (TM_from_str "<tm>") c0`), fully qualified, both inside a temp
#       copy of the file and in a separate checker that never imports the file;
#   (d) no forbidden token (ground rule 1's words anywhere, comments and strings
#       included; dangerous command words anywhere outside comments and strings; a
#       comment never splits a token) and a clean structure (Require allowlist, no
#       top-level Variable/Context, no Fail/Succeed, no re-binding of tm/c0/halts/
#       TM_from_str/the theorem name, balanced modules);
#   (e) `Print Assumptions` of the theorem lists nothing outside
#       tools/assumptions_baseline.txt (written by tools/make_baseline.sh), compared
#       entry by entry (name and type), and nothing declared by the file itself;
#   (f) the temp copy compiles with flags mirroring verify/_CoqProject within the
#       timeout (default 1800 s), from a temp directory outside vendor/, with
#       -native-compiler yes as in _CoqProject unless --native says otherwise;
#   (g) the isolated checker loads no ML plugin beyond the stock proof plugins and
#       runs with guard/positivity/universe checking on and definitional UIP off;
#   (h) coqchk re-checks the compiled candidate (independent kernel; also re-checks
#       every vm_compute/native_compute step by plain conversion), and its context
#       summary (-o) lists no axiom, unsafe fixpoint, type-in-type or assumed positivity
#       of the file's own. --no-coqchk skips it. Policy A (Dennis, 2026-10-09): coqchk
#       has its own time cap (--coqchk-timeout, default 600 s); a coqchk TIMEOUT is a
#       warning and still allows PASS (the RESULT line and the JSON say so), but any
#       coqchk error or finding is a FAIL, also one printed before the timeout.
# Trust (policy A): coqc's kernel checks every Qed; vm_compute/native_compute steps are
# checked by the VM / by native code generated at compile time, the same trust upstream's
# accepted proofs rely on. Only a finished coqchk re-checks those steps independently; a
# PASS after a coqchk timeout rests on coqc alone.
# The input file is never modified: every check runs on a private temp copy.
#
# options:
#   --halt                 prove halting: theorem `halt : halts tm c0`
#   --name NAME            theorem name (default nonhalt, or halt with --halt)
#   --timeout SEC          compile timeout for the candidate (default 1800, at most 604800)
#   --json                 print only the JSON summary on stdout (report goes to stderr)
#   --text-only            run only the checks that need no Coq (dry run); exit 4 if
#                          they all pass. Never a kill verdict.
#   --native MODE          -native-compiler for the candidate (yes|no|ondemand). Default
#                          yes, as in verify/_CoqProject ($CHECK_KILL_NATIVE overrides):
#                          native_compute steps are then checked by generated OCaml code
#                          that Print Assumptions never mentions, the same trust upstream
#                          accepts. `no` falls back to the VM (~4.7x slower on Bouncer_v3).
#   --coqchk-timeout SEC   time cap for check (h) (default 600, at most 604800). A timeout
#                          is a warning, not a failure (policy A); reported in the JSON as
#                          "timeout" and on the RESULT line.
#   --no-coqchk            skip check (h) (JSON "coqchk": false; VM and native results
#                          then get no second check)
#   --coqchk               accepted for compatibility (coqchk is on by default)
#   --keep                 keep the temp directory and print its path
#   --emit-assumptions F   (for make_baseline.sh) write the isolated checker's raw
#                          Print Assumptions output to F and skip the baseline
#                          comparison; exits 3 when everything else passed. Never a kill
#                          verdict.
#   --selftest             (for test_check_kill.sh) compile even when text checks
#                          failed, so the Rocq-level layers can be tested on their own;
#                          refuses files with dangerous commands. Exits 5 at best.
# exit codes: 0 PASS (the only kill signal) | 1 FAIL | 2 usage/internal error, also
#             --help | 3 BASELINE_SKIPPED | 4 TEXT_ONLY_OK | 5 SELFTEST_OK
#             | 128+N killed by signal N (SIGTERM/SIGHUP: coqc and the temp dir are
#             cleaned up first)
# environment: COQC, COQCHK (tool paths), CHECK_KILL_TMPDIR (temp base),
#              CHECK_KILL_NATIVE (default for --native). coqc runs with PATH = coqc's bin
#              directory + the absolute entries of PATH, without OCAMLPARAM/OCAMLFIND_*.
# JSON summary: the fields, and the values of "coqchk", are listed at TOOL_VERSION below.
#
# The logic is the Python program below (stdlib only, run isolated with -I); bash
# only locates it. Design notes: atlas/rocq-notes.md, "Framework anatomy (for check_kill)".
set -euo pipefail
unset CDPATH   # a set CDPATH makes `cd` print the directory, corrupting $(...) below
self=$(readlink -f -- "${BASH_SOURCE[0]}")   # resolve symlinks (e.g. ~/bin/check_kill)
root=$(cd -P -- "$(dirname -- "$self")/.." > /dev/null && pwd -P)
if ! command -v python3 >/dev/null 2>&1; then
  echo "check_kill: python3 not found on PATH" >&2
  exit 2
fi
# Accepted upstream proofs (e.g. Bouncer_v3.v) overflow coqc's stack at the default 8 MB.
ulimit -s unlimited 2>/dev/null || ulimit -s "$(ulimit -H -s)"
exec python3 -I - "$root" "$@" <<'CHECK_KILL_PY'
import datetime
import glob
import hashlib
import json
import os
import re
import secrets
import shlex
import shutil
import signal
import subprocess
import sys
import tempfile
import time

TOOL_VERSION = 4   # 4: coqchk enum (pass|timeout|fail|not_run|false), coqchk_timeout, coqchk_seconds
# JSON summary (the last stdout line, after "JSON: "; all of stdout with --json):
#   result, exit           the verdict; exit 0 <=> result PASS, and only that is a kill
#   native_compiler        yes|no|ondemand (null if the Coq phase stopped before compiling)
#   coqchk                 what check (h) did:
#     "pass"       coqchk finished and lists nothing of the file's own
#     "timeout"    coqchk hit --coqchk-timeout and had printed no error or finding so far:
#                  SKIP, which still allows PASS (policy A)
#     "fail"       check (h) failed: a coqchk error or finding (also one printed before a
#                  timeout), coqchk not found, no compiled candidate to check, or an
#                  internal error
#     "not_run"    the Coq phase stopped before (h) (an earlier check failed or was skipped)
#     false        (h) is off: --no-coqchk or --text-only
#   coqchk_timeout         the cap in seconds (null when "coqchk" is false)
#   coqchk_seconds         coqchk's wall time (null when it never ran)
#   checks                 every check: id, status (PASS|FAIL|SKIP), summary, details, warnings
COQCHK_OUTCOMES = {"pass": "PASS", "timeout": "SKIP", "fail": "FAIL", "not_run": "SKIP"}   # -> status of (h)
MAX_TIMEOUT = 604800       # one week: larger --timeout values overflow subprocess's timer
NATIVE_MODES = ("yes", "no", "ondemand")
ROOT = os.path.realpath(sys.argv[1])
ARGS = sys.argv[2:]
VENDOR = os.path.join(ROOT, "vendor", "busycoq")
VERIFY = os.path.join(VENDOR, "verify")
PIN_FILE = os.path.join(ROOT, "tools", "busycoq.pin")
BASELINE_FILE = os.path.join(ROOT, "tools", "assumptions_baseline.txt")
LIB = "BB6Kill"            # logical root bound to the temp directory
CAND = "Candidate"         # module name of the temp copy (machine names are not valid Coq idents)
CHECKER = "CheckKill"      # isolated checker module
PROBE_LIB = "BB6KillProbe"
IDENT = r"[A-Za-z_][A-Za-z0-9_']*"
QUALID = IDENT + r"(?:\." + IDENT + r")*"

USAGE = """usage: tools/check_kill.sh [--halt] [--name NAME] [--timeout SEC] [--json]
                            [--text-only] [--native MODE] [--coqchk-timeout SEC]
                            [--no-coqchk] [--keep]
                            [--emit-assumptions FILE] [--selftest] <file.v> <tm>
(see the header of tools/check_kill.sh for details; exit 0 means a kill and nothing else,
so --help exits 2)"""

# Shapes check_kill understands. Only (6,2) matters for BB(6); the others let the
# oracle be exercised on the repo's 2x5 / 3x3 proofs.
SHAPES = {
    (6, 2): {"module": "Individual62", "states": "ABCDEF", "syms": "01"},
    (2, 5): {"module": "Individual25", "states": "AB", "syms": "01234"},
    (3, 3): {"module": "Individual33", "states": "ABC", "syms": "012"},
}


def expected_fqns(mod):
    # Individual<NN>.v: `Module <M> := Individual <Ctx>.` -> Individual: `Module Enumerate :=`
    # -> Enumerate: `Module Permute :=` -> Permute: `Module Flip :=` -> Flip: `Module Compute :=`
    # -> Compute: `Module TM := TM Ctx.` (TM.v defines halts and c0). TM_from_str is a
    # top-level definition of Individual<NN>.v itself. The probe confirms these at run time.
    tmmod = "BusyCoq.%s.%s.Enumerate.Permute.Flip.Compute.TM" % (mod, mod)
    return {"halts": tmmod + ".halts", "c0": tmmod + ".c0",
            "TM_from_str": "BusyCoq.%s.TM_from_str" % mod}


# ----------------------------------------------------------------------------------------
# (d) forbidden tokens: case-sensitive regexes. Each entry: (regex, reason, scope, dangerous).
# Coq reads a comment as a space, so `Unset Guard (* x *) Checking.` is the command
# `Unset Guard Checking.`: every regex is therefore also run on text whose comments are
# blanked to spaces, where `\s+` spans them.
#   scope "spec": ground rule 1's list (and its synonyms) plus check_kill's reserved names.
#       Strict: matched on the raw text (comments and strings included, since that is where
#       a reviewer could be misled) AND on the comment-blanked code.
#   scope "cmd": words that only do something as commands. Matched on the code with
#       comments AND string contents blanked; an occurrence inside a comment or a string is
#       reported as a warning only (`(* Load phase: ... *)` is prose, not a command).
# "dangerous" ones also block running coqc at all, because they can execute code or touch
# files during compilation.
FORBIDDEN = [
    (r"\bAdmitted\b", "Admitted: the statement is accepted without proof (becomes an axiom)", "spec", False),
    (r"\badmit\b", "admit: closes a goal without proof", "spec", False),
    (r"\bAxioms?\b", "Axiom(s): unproven assumption", "spec", False),
    (r"\bParameters?\b", "Parameter(s): synonym of Axiom", "spec", False),
    (r"\bHypothes(?:is|es)\b", "Hypothesis/Hypotheses: an axiom at top level (banned outright by ground rule 1)",
     "spec", False),
    (r"\bConjectures?\b", "Conjecture: synonym of Axiom", "spec", False),
    (r"\bAbort\b", "Abort: abandoned proof attempt; never part of a finished kill", "spec", False),
    (r"\bbypass_check\b", "#[bypass_check(...)]: disables kernel guard/positivity/universe checks", "spec", False),
    (r"\bGuard\s+Checking\b", "Guard Checking flag: Unset makes the kernel accept non-terminating fixpoints",
     "spec", False),
    (r"\bBB6Kill\w*", "reserved for check_kill's own checks (BB6Kill namespace)", "spec", False),
    (r"\bCHECK_KILL\w*", "reserved for check_kill's appended checks", "spec", False),
    (r"\bAdmit\b", "Admit Obligations: admits Program obligations", "cmd", False),
    (r"\bgive_up\b", "give_up: abandons goals", "cmd", False),
    (r"\bPositivity\s+Checking\b", "Positivity Checking flag: Unset admits inconsistent inductive types", "cmd", False),
    (r"\bUniverse\s+Checking\b", "Universe Checking flag: Unset admits Type:Type (inconsistent)", "cmd", False),
    (r"\b(?:Set|Unset)\s+[A-Z][A-Za-z\s]*?\s+Checking\b", "changes a kernel checking flag", "cmd", False),
    (r"\bDefinitional\s+UIP\b", "Definitional UIP: extends the logic", "cmd", False),
    (r"\bDeclare\s+(?:Module|Instance|Morphism)\b", "Declare Module/Instance/Morphism: declares its fields or "
     "itself as axioms (a Parameter synonym); never needed in a kill", "cmd", False),
    (r"\bInclude\b", "Include: including a module type declares its fields as axioms (a Parameter synonym); "
     "never needed in a kill", "cmd", False),
    (r"\bDeclare\s+ML\b", "Declare ML Module: loads an OCaml plugin, i.e. arbitrary code inside the checker",
     "cmd", True),
    (r"\bML\s+(?:Path|Module)\b", "ML Path/Module: plugin loading", "cmd", True),
    (r"\bLoad\b", "Load: splices another file's commands in, bypassing this scan", "cmd", True),
    (r"\bLoadPath\b", "Add (Rec) LoadPath: changes which files Require resolves to", "cmd", True),
    (r"\bExtract\b", "Extract Constant/Inductive: realizers; never needed in a kill", "cmd", True),
    (r"\bExtraction\b", "Extraction: writes files and pulls in the extraction plugin; never needed in a kill",
     "cmd", True),
    (r"\bRedirect\b", "Redirect: writes command output to files", "cmd", True),
    (r"\bRegister\b", "Register: rebinds kernel/tactic hooks (kernel.ind_*, core.*)", "cmd", True),
    (r"\bPrimitive\b(?!\s+Projections\b)", "Primitive: declares kernel primitives (`Primitive Projections` "
     "is fine)", "cmd", True),
    (r"\bReset\b", "Reset: rewinds the environment; never part of a finished kill", "cmd", False),
    (r"\bBackTo\b", "BackTo: rewinds the environment", "cmd", False),
]

# Sentence prefixes that run a command and then roll it back. A finished kill never needs
# them, and with them what the text says (a `Definition tm`, an open Section) is not what
# Coq keeps, so they are a structure failure.
ROLLBACK_RE = re.compile(r"\b(?:Fail|Succeed)\b")

# (g) ML plugins the isolated checker may see loaded: the stock plugins that the allowed
# Requires (Coq stdlib, BusyCoq) use. Anything else (third-party plugins, extraction, the
# tutorial plugin) is OCaml code running inside the checker and fails the kill.
STOCK_PLUGINS = {"ltac", "tauto", "cc", "firstorder", "number_string_notation", "ring", "zify",
                 "micromega", "micromega_core", "btauto", "nsatz", "rtauto", "funind", "derive",
                 "ssreflect", "ssrmatching"}
# (g) `Print Typing Flags` in the isolated checker must read exactly this (Coq 8.20).
EXPECTED_TYPING_FLAGS = ["check_guarded: true", "check_positive: true", "check_universes: true",
                         "definitional uip: false"]
# (e) Print Assumptions entries that are failures whatever the baseline says: kernel
# checks that were switched off, and assumptions declared by the candidate itself.
UNSAFE_ENTRY_RE = re.compile(r"is assumed to be (?:guarded|positive)|relies on (?:an unsafe hierarchy|"
                             r"definitional UIP|rewrite rules)")
OWN_NAME_RE = re.compile(r"(?:BB6Kill\.)?(?:Candidate|CheckKill)\.")

# Command-position checks (on comment-stripped sentences).
DANGEROUS_COMMANDS = {
    "Cd": "Cd: changes the working directory of coqc",
    "Drop": "Drop: leaves the Coq loop",
    "Quit": "Quit: stops compilation early",
    "Back": "Back: rewinds the environment",
}

# Bare `Require <name>` (no From) is accepted only for these Coq standard library
# names (gathered from the names verify/ actually uses plus common stdlib modules), or
# for names that resolve to a TRACKED file of verify/. Anything else must be written
# `From Coq Require ...` / `Require Coq.X.Y`, so a third-party library in user-contrib
# can never be pulled in by an ambiguous short name.
STDLIB_BARE = set("""
Lia Lra Psatz Zify ZifyNat ZifyN ZifyBool ZifyUint63 ZifySint63 ZifyClasses ZifyInst ZifyComparison
ZArith NArith PArith QArith Arith Arith_base PeanoNat Nat BinNat BinInt BinPos BinNums BinList
Znat Nnat Pnat Zdiv Zpow_facts Zbool Zcompare Zeven Zmax Zmin Zminmax Zorder ZArith_dec Zwf Znumtheory
Wf_nat Wf Compare_dec EqNat Even Div2 Peano_dec Max Min Euclid Factorial Cantor
Bool Bvector Sumbool DecBool IfProp Ascii String Byte HexString
List ListDec ListSet SetoidList Streams Permutation Sorted Sorting Mergesort Orders OrdersFacts
OrderedType OrderedTypeEx FMapPositive FMapAVL FMapList FMapInterface FMaps FSets MSets
Uint63 Sint63 PrimInt63 PArray PrimArray Int63
Relations Relation_Definitions Relation_Operators Operators_Properties Setoid Morphisms
RelationClasses Equivalence SetoidTactics Ring Field Ring_theory Field_theory
FunInd Recdef Program Equality Utf8 Utf8_core Decidable Eqdep_dec EqdepFacts Eqdep JMeq
ProofIrrelevance FunctionalExtensionality Classical ClassicalFacts Classical_Prop
Lists.List Lists.Streams Lists.ListSet Lists.SetoidList Arith.PeanoNat Arith.Arith Arith.Compare_dec
Arith.Wf_nat Bool.Bool Bool.Sumbool Strings.String Strings.Ascii Program.Tactics Program.Equality
Program.Basics Logic.FunctionalExtensionality Logic.ProofIrrelevance Logic.Eqdep_dec Logic.Eqdep
Logic.JMeq Logic.Classical micromega.Lia micromega.Zify micromega.ZifyClasses micromega.Psatz
Classes.Morphisms Classes.RelationClasses Classes.SetoidTactics Classes.Equivalence
FSets.FMapPositive FSets.FMapAVL FSets.FMapList NArith.BinNat NArith.Nnat PArith.BinPos PArith.Pnat
ZArith.BinInt ZArith.Znat Numbers.BinNums Init.Nat
""".split())
STDLIB_ROOTS = {"Coq", "Stdlib", "Corelib"}


class UsageError(Exception):
    pass


# ======================================================================== report
class Report:
    STATUSES = ("PASS", "FAIL", "SKIP")

    def __init__(self):
        self.order = []
        self.checks = {}
        self.meta = {}

    def add(self, cid, title):
        self.order.append(cid)
        self.checks[cid] = {"id": cid, "title": title, "status": "SKIP",
                            "summary": "not run", "details": [], "warnings": []}

    def set(self, cid, status, summary, details=None):
        assert status in self.STATUSES, status
        c = self.checks[cid]
        c["status"], c["summary"] = status, summary
        if details:
            c["details"].extend(details)

    def detail(self, cid, line):
        self.checks[cid]["details"].append(line)

    def warn(self, cid, line):
        self.checks[cid]["warnings"].append(line)

    def status(self, cid):
        return self.checks[cid]["status"]

    def failed(self):
        return [c for c in self.order if self.checks[c]["status"] == "FAIL"]


# ======================================================================== utilities
def sha256_bytes(b):
    return hashlib.sha256(b).hexdigest()


def is_within(path, parent):
    path, parent = os.path.realpath(path), os.path.realpath(parent)
    return path == parent or path.startswith(parent + os.sep)


def git(*args, check=False):
    env = dict(os.environ, GIT_OPTIONAL_LOCKS="0", LC_ALL="C")  # never write vendor/.git/index
    p = subprocess.run(["git", "-C", VENDOR] + list(args), stdout=subprocess.PIPE,
                       stderr=subprocess.PIPE, env=env, stdin=subprocess.DEVNULL)
    if check and p.returncode != 0:
        raise RuntimeError("git %s failed: %s" % (" ".join(args), p.stderr.decode(errors="replace").strip()))
    return p


try:
    import ctypes
    _PRCTL = ctypes.CDLL(None, use_errno=True).prctl   # Linux only; best effort
except (ImportError, OSError, AttributeError):
    _PRCTL = None


def _dies_with(parent_pid):
    """preexec_fn: the child (coqc) gets SIGKILL if check_kill itself dies, even by SIGKILL."""
    def setup():
        if _PRCTL is not None:
            _PRCTL(1, signal.SIGKILL)   # 1 = PR_SET_PDEATHSIG
        if os.getppid() != parent_pid:  # check_kill died before prctl took effect
            os._exit(1)
    return setup


def run_proc(cmd, cwd, timeout, env=None):
    """Run cmd in its own process group; kill the whole group on timeout, and also when
    check_kill is interrupted (Ctrl-C, or SIGTERM/SIGHUP, which main turns into SystemExit)."""
    t0 = time.monotonic()
    p = subprocess.Popen(cmd, cwd=cwd, env=env, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
                         stderr=subprocess.PIPE, start_new_session=True, preexec_fn=_dies_with(os.getpid()))
    timed_out = False
    try:
        try:
            out, err = p.communicate(timeout=timeout)
        except subprocess.TimeoutExpired:
            timed_out = True
            for sig in (signal.SIGTERM, signal.SIGKILL):
                try:
                    os.killpg(p.pid, sig)
                except ProcessLookupError:
                    pass
                try:
                    out, err = p.communicate(timeout=20)
                    break
                except subprocess.TimeoutExpired:
                    continue
            else:
                out, err = b"", b""
    finally:
        if p.returncode is None:   # not reaped: still running (we are being interrupted)
            try:
                os.killpg(p.pid, signal.SIGKILL)
            except ProcessLookupError:
                pass
    return {"rc": p.returncode, "out": out.decode("utf-8", errors="replace"),
            "err": err.decode("utf-8", errors="replace"), "seconds": round(time.monotonic() - t0, 2),
            "timed_out": timed_out}


def tail(text, n=25):
    lines = [l for l in text.rstrip().splitlines()]
    return lines[-n:]


# ======================================================================== Coq lexing
def skip_string(src, i):
    """src[i] == '"'. Return the index just past the closing quote ("" escapes a quote)."""
    j, n = i + 1, len(src)
    while j < n:
        if src[j] == '"':
            if j + 1 < n and src[j + 1] == '"':
                j += 2
                continue
            return j + 1
        j += 1
    return None


def lex(src):
    """Blank out comments (nested; strings inside comments respected) keeping offsets and
    newlines. Return (code, code_nostr, string_spans, comment_spans, errors), where
    code_nostr is code with the contents of string literals blanked as well."""
    code = list(src)
    strings, comments, errors = [], [], []
    i, n = 0, len(src)
    while i < n:
        if src.startswith("(*", i):
            start, depth, j = i, 1, i + 2
            while j < n and depth:
                if src.startswith("(*", j):
                    depth, j = depth + 1, j + 2
                elif src.startswith("*)", j):
                    depth, j = depth - 1, j + 2
                elif src[j] == '"':
                    k = skip_string(src, j)
                    if k is None:
                        errors.append(("unterminated string inside a comment", j))
                        j = n
                        break
                    j = k
                else:
                    j += 1
            if depth:
                errors.append(("unterminated comment", start))
            end = min(j, n)
            for k in range(start, end):
                if code[k] != "\n":
                    code[k] = " "
            comments.append((start, end))
            i = end
        elif src[i] == '"':
            k = skip_string(src, i)
            if k is None:
                errors.append(("unterminated string", i))
                strings.append((i, n))
                i = n
            else:
                strings.append((i, k))
                i = k
        else:
            i += 1
    nostr = list(code)
    for (s, e) in strings:
        for k in range(s + 1, e - 1):
            if nostr[k] != "\n":
                nostr[k] = " "
    return "".join(code), "".join(nostr), strings, comments, errors


def split_sentences(code, strings):
    """Coq sentences end with '.' followed by whitespace or EOF (outside strings)."""
    str_end = dict(strings)
    sents, start, i, n = [], 0, 0, len(code)
    while i < n:
        if i in str_end:
            i = str_end[i]
            continue
        if code[i] == "." and (i + 1 == n or code[i + 1].isspace()):
            sents.append((start, i + 1))
            start = i + 1
        i += 1
    trailing = code[start:].strip()
    return sents, trailing


PREFIX_RE = re.compile(r"\A(?:#\[[^\]]*\]\s*|(?:Local|Global|Export|Polymorphic|Monomorphic|Cumulative|"
                       r"NonCumulative|Private|Program|Time|Fail|Succeed|Timeout\s+\d+|Instructions|Profile)\b\s*)+")


def command_head(text):
    """Strip whitespace, bullets, braces, goal selectors, then attributes and locality/control
    prefixes. Return (head, prefix) where prefix is the stripped attribute/prefix text."""
    prev = None
    t = text
    while prev != t:
        prev = t
        t = t.lstrip()
        t = re.sub(r"\A(?:[-+*]+|[{}])", "", t)
        t = re.sub(r"\A(?:\d+(?:\s*[-,]\s*\d+)*|all|par|!)\s*:(?!=)", "", t)
    m = PREFIX_RE.match(t)
    return (t[m.end():], m.group(0)) if m else (t, "")


class Sentence:
    __slots__ = ("start", "end", "text", "head", "prefix", "depth", "in_section", "line")


class Analysis:
    pass


def line_of(line_starts, pos):
    lo, hi = 0, len(line_starts) - 1
    while lo < hi:
        mid = (lo + hi + 1) // 2
        if line_starts[mid] <= pos:
            lo = mid
        else:
            hi = mid - 1
    return lo + 1


def analyze(src):
    a = Analysis()
    a.src = src
    a.line_starts = [0] + [m.end() for m in re.finditer("\n", src)]
    a.code, a.code_nostr, a.strings, a.comments, a.lex_errors = lex(src)
    spans, a.trailing = split_sentences(a.code, a.strings)
    a.sentences, a.struct_errors = [], []
    stack = []
    for (s, e) in spans:
        st = Sentence()
        st.start, st.end = s, e
        st.text = a.code[s:e]
        st.head, st.prefix = command_head(st.text)
        st.depth = len(stack)
        st.in_section = any(k == "Section" for k, _ in stack)
        st.line = line_of(a.line_starts, s + (len(st.text) - len(st.text.lstrip())))
        a.sentences.append(st)
        if ROLLBACK_RE.search(st.prefix):
            continue   # rolled back by Coq: no structural effect (and a structure failure)
        h = st.head
        m = re.match(r"Section\s+(" + IDENT + r")", h)
        if m:
            stack.append(("Section", m.group(1)))
            continue
        m = re.match(r"Module\s+(?:Type\s+)?(?:(?:Import|Export)\s+)?(" + IDENT + r")", h)
        if m and ":=" not in h:
            stack.append(("Module", m.group(1)))
            continue
        m = re.match(r"End\s+(" + IDENT + r")\s*\.\Z", h)
        if m:
            if not stack:
                a.struct_errors.append((st.line, "`End %s` without an open Module/Section" % m.group(1)))
            elif stack[-1][1] != m.group(1):
                a.struct_errors.append((st.line, "`End %s` closes %s %s" % (m.group(1), stack[-1][0], stack[-1][1])))
                stack.pop()
            else:
                stack.pop()
    a.open_at_eof = list(stack)
    return a


def strings_in(a, s, e):
    return [(x, y) for (x, y) in a.strings if s <= x and y <= e]


def decode_literal(src, span):
    x, y = span
    return src[x + 1:y - 1].replace('""', '"')


# ======================================================================== checks
def check_tm_format(tm):
    """Return (shape, problems, warnings)."""
    problems, warnings = [], []
    if not tm or not re.fullmatch(r"[0-9A-Z_-]+", tm):
        return None, ["TM string must match [0-9A-Z_-]+ (got %r)" % tm], warnings
    groups = tm.split("_")
    if any(len(g) == 0 or len(g) % 3 for g in groups):
        return None, ["every `_`-separated group must be a multiple of 3 characters"], warnings
    nsyms = {len(g) // 3 for g in groups}
    if len(nsyms) != 1:
        return None, ["groups have different numbers of transitions"], warnings
    shape = (len(groups), nsyms.pop())
    if shape not in SHAPES:
        return None, ["unsupported shape %d states x %d symbols (supported: %s)" % (
            shape[0], shape[1], ", ".join("%dx%d" % k for k in SHAPES))], warnings
    states, syms = SHAPES[shape]["states"], SHAPES[shape]["syms"]
    for gi, g in enumerate(groups):
        for k in range(0, len(g), 3):
            t = g[k:k + 3]
            if t == "---":
                continue
            if t[0] in syms and t[1] in "LR" and (t[2] in states or t[2] == "Z"):
                if t[2] == "Z":
                    warnings.append("transition %s uses Z (TM_from_str maps it to halt, like ---)" % t)
                continue
            problems.append("bad transition %r in state %s" % (t, "ABCDEFGH"[gi]))
    return (shape if not problems else None), problems, warnings


def framework_state():
    st = {"ok": True, "problems": [], "head": None, "untracked": [], "tracked_v": []}
    if not os.path.isdir(os.path.join(VENDOR, ".git")) and not os.path.isfile(os.path.join(VENDOR, ".git")):
        st["ok"] = False
        st["problems"].append("vendor/busycoq is not a git checkout")
        return st
    try:
        pin = open(PIN_FILE, encoding="utf-8").read().strip()
    except OSError:
        st["ok"] = False
        st["problems"].append("missing tools/busycoq.pin (one line: the pinned busycoq commit hash)")
        pin = None
    if pin is not None and not re.fullmatch(r"[0-9a-f]{40}", pin):
        st["ok"] = False
        st["problems"].append("tools/busycoq.pin is not a 40-hex commit hash: %r" % pin[:60])
        pin = None
    p = git("rev-parse", "HEAD")
    if p.returncode != 0:
        st["ok"] = False
        st["problems"].append("git rev-parse HEAD failed: " + p.stderr.decode(errors="replace").strip())
    else:
        st["head"] = p.stdout.decode().strip()
        if pin and st["head"] != pin:
            st["ok"] = False
            st["problems"].append("vendor/busycoq HEAD %s != pin %s" % (st["head"], pin))
    st["pin"] = pin
    p = git("diff", "--quiet", "HEAD", "--", "verify")
    if p.returncode == 1:
        st["ok"] = False
        names = git("diff", "--name-only", "HEAD", "--", "verify").stdout.decode(errors="replace").split()
        st["problems"].append("tracked files under verify/ differ from HEAD: " + ", ".join(names[:12]) +
                              (" ..." if len(names) > 12 else ""))
    elif p.returncode != 0:
        st["ok"] = False
        st["problems"].append("git diff failed: " + p.stderr.decode(errors="replace").strip())
    p = git("ls-files", "-z", "--", "verify")
    if p.returncode == 0:
        st["tracked_v"] = [x for x in p.stdout.decode(errors="replace").split("\0") if x.endswith(".v")]
    else:
        st["ok"] = False
        st["problems"].append("git ls-files failed")
    p = git("ls-files", "-z", "--others", "--exclude-standard", "--", "verify")
    if p.returncode == 0:
        st["untracked"] = [x for x in p.stdout.decode(errors="replace").split("\0") if x]
    return st


def build_index(tracked_v):
    """Logical paths of tracked framework files: verify/X/Y.v -> BusyCoq.X.Y (and BigInt.Y)."""
    idx = []
    for rel in tracked_v:
        if not rel.startswith("verify/"):
            continue
        r = rel[len("verify/"):]
        comps = r[:-2].split("/")
        idx.append((tuple(["BusyCoq"] + comps), r))
        if comps[0] == "BigInt" and len(comps) > 1:
            idx.append((tuple(["BigInt"] + comps[1:]), r))
    return idx


def resolve(idx, root, comps):
    out = set()
    comps = tuple(comps)
    for lp, rel in idx:
        if root is not None:
            if lp[0] == root and len(lp) >= len(comps) + 1 and lp[-len(comps):] == comps:
                out.add(rel)
        elif len(lp) >= len(comps) and lp[-len(comps):] == comps:
            out.add(rel)
    return sorted(out)


REQ_RE = re.compile(r"\A(?:From\s+(" + QUALID + r")\s+)?Require\b\s*(?:(?:Import|Export)\b\s*)?"
                    r"(?:-?\(\s*[^)]*\)\s*)?(.*?)\s*\.\Z", re.S)


def parse_requires(a):
    """Return list of (line, root, name) and list of (line, problem)."""
    reqs, bad = [], []
    for st in a.sentences:
        if not re.search(r"\bRequire\b", st.head):
            continue
        m = REQ_RE.match(st.head)
        if not m:
            bad.append((st.line, "unparseable Require sentence: %s" % " ".join(st.head.split())[:120]))
            continue
        root, rest = m.group(1), m.group(2)
        names = rest.split()
        if not names:
            bad.append((st.line, "Require with no module names"))
        for nm in names:
            if not re.fullmatch(QUALID, nm):
                bad.append((st.line, "unparseable module name %r in Require" % nm))
                continue
            reqs.append((st.line, root, nm))
    return reqs, bad


def classify_require(idx, root, name):
    """Return ('stdlib'|'framework'|'reject', [rel paths], reason)."""
    comps = name.split(".")
    if root is not None:
        if root in STDLIB_ROOTS:
            return "stdlib", [], ""
        if root in ("BusyCoq", "BigInt"):
            hits = resolve(idx, root, comps)
            if hits:
                return "framework", hits, ""
            return "reject", [], "From %s Require %s: no tracked file under vendor/busycoq/verify matches" % (root, name)
        return "reject", [], "From %s Require ...: only Coq stdlib, BusyCoq and BigInt are allowed" % root
    if comps[0] in STDLIB_ROOTS and len(comps) > 1:
        return "stdlib", [], ""
    if comps[0] in ("BusyCoq", "BigInt") and len(comps) > 1:
        hits = resolve(idx, comps[0], comps[1:])
        if hits:
            return "framework", hits, ""
        return "reject", [], "Require %s: no tracked file under vendor/busycoq/verify matches" % name
    if name in STDLIB_BARE:
        return "stdlib", [], ""
    hits = resolve(idx, None, comps)
    if hits:
        return "framework", hits, ""
    return "reject", [], ("bare `Require %s` is not on the stdlib allowlist and is no tracked framework file; "
                          "write `From Coq Require ...`" % name)


def framework_closure(idx, start_rels):
    """Transitive closure of framework files needed by start_rels (by parsing their Requires)."""
    seen, todo = set(), list(start_rels)
    while todo:
        rel = todo.pop()
        if rel in seen:
            continue
        seen.add(rel)
        try:
            src = open(os.path.join(VERIFY, rel), encoding="utf-8", errors="replace").read()
        except OSError:
            continue
        reqs, _ = parse_requires(analyze(src))
        for _, root, name in reqs:
            kind, hits, _ = classify_require(idx, root, name)
            if kind == "framework":
                todo.extend(h for h in hits if h not in seen)
    return sorted(seen)


# Commands whose FIRST identifier is the global name they bind (the identifiers after it,
# as in `Lemma halts_id tm c0 : ...`, are local binders). `Arguments` re-declares how an
# existing name is applied, which is as good as re-binding it for this check.
FIRST_NAME_CMD = re.compile(
    r"(?:Definition|Let|Fixpoint|CoFixpoint|Lemma|Theorem|Corollary|Proposition|Fact|Remark|Example|"
    r"Property|Instance|Function|Equations|Abbreviation|Inductive|CoInductive|Variant|Record|Structure|"
    r"Class|Canonical(?:\s+Structure)?|Coercion|Scheme|Combined\s+Scheme|Functional\s+Scheme|Derive|"
    r"Add\s+(?:Ring|Field)|Arguments)\s+(" + IDENT + r")")
# Commands where EVERY identifier before the type is declared (`Variables x y : T`,
# `Context (x : T) {y : U}`).
ALL_NAMES_CMD = re.compile(r"(?:Axioms?|Parameters?|Conjectures?|Variables?|Hypothes(?:is|es)|Context)\b(.*)", re.S)
TYPE_CMD = re.compile(r"(?:Inductive|CoInductive|Variant|Record|Structure|Class)\b")


def notation_hits(ntext, names):
    hits = []
    for tok in ntext.split():
        if tok.strip("'") in names:
            hits.append(tok.strip("'"))
        if "~" in tok:
            hits.append("~")
    return hits


def shadow_hits(head, names):
    """Names (from `names`, plus "~") that this command binds as a global or section name,
    re-declares, or turns into notation tokens."""
    found, hits = [], []
    m = FIRST_NAME_CMD.match(head)
    if m:
        found.append(m.group(1))
        found += re.findall(r"\bwith\s+(" + IDENT + r")", head)          # mutual blocks
    if TYPE_CMD.match(head):
        found += re.findall(r"(?::=|\|)\s*(" + IDENT + r")", head)        # constructors, class field
        found += re.findall(r"[{;]\s*(" + IDENT + r")\s*:", head)         # record fields
    if re.match(r"(?:Derive|Add)\b", head):
        found += re.findall(r"\b(?:As|as)\s+(" + IDENT + r")", head)      # Derive ... As, Add ... as
    m = ALL_NAMES_CMD.match(head)
    if m:
        rest = m.group(1).lstrip()
        groups = (re.findall(r"[(\[{`]+\s*([^:(){}\[\]]*?)\s*:", rest) if rest[:1] in "({[`"
                  else [rest.split(":", 1)[0]])
        for g in groups:
            found += re.findall(IDENT, g)
    hits += [n for n in found if n in names]
    m = re.match(r"(?:Reserved\s+)?(?:Notation|Infix)\s+(.*)", head, re.S)
    if m:
        rest = m.group(1).lstrip()
        if rest.startswith('"'):
            k = skip_string(rest, 0)
            hits += notation_hits(rest[1:(k - 1) if k else len(rest)].replace('""', '"'), names)
        else:
            mm = re.match(IDENT, rest)
            if mm and mm.group(0) in names:
                hits.append(mm.group(0))
    for w in re.finditer(r"\bwhere\s+\"", head):                          # `Inductive ... where "x ~ y" := ...`
        k = skip_string(head, w.end() - 1)
        hits += notation_hits(head[w.end():(k - 1) if k else len(head)].replace('""', '"'), names)
    return hits


def run_text_checks(rep, a, tm, thm, mode, idx, ctx):
    """forbidden, structure, tm_text, theorem_text. Fills ctx['dangerous'], ctx['fw_modules']."""
    src = a.src
    in_comment = [False] * (len(src) + 1)
    for (s, e) in a.comments:
        for k in range(s, e):
            in_comment[k] = True
    in_string = [False] * (len(src) + 1)
    for (s, e) in a.strings:
        for k in range(s, e):
            in_string[k] = True

    # ---- (d) forbidden tokens (see FORBIDDEN for the two scopes)
    def show(pos, tok):
        ln = line_of(a.line_starts, pos)
        where = "comment" if in_comment[pos] else ("string" if in_string[pos] else "code")
        if src[pos:pos + len(tok)] != tok:
            where += ", split by a comment"
        line_text = src[a.line_starts[ln - 1]:].split("\n", 1)[0].strip()
        return ln, where, " ".join(tok.split()), line_text[:100]

    hits, dangerous = [], []
    for rx, why, scope, danger in FORBIDDEN:
        found = {}   # match start -> matched text, de-duplicated across the texts scanned
        for text in ((src, a.code) if scope == "spec" else (a.code_nostr,)):
            for m in re.finditer(rx, text):
                found.setdefault(m.start(), m.group(0))
        for pos, tok in sorted(found.items()):
            ln, where, tok, line_text = show(pos, tok)
            hits.append("line %d (%s): `%s` -- %s  | %s" % (ln, where, tok, why, line_text))
            if danger:
                dangerous.append("line %d: %s" % (ln, tok))
        if scope == "cmd":
            for m in re.finditer(rx, src):
                if m.start() not in found:
                    ln, where, tok, _ = show(m.start(), m.group(0))
                    rep.warn("forbidden", "line %d (%s): `%s` is not a command there, so it is allowed" % (ln, where, tok))
    if hits:
        rep.set("forbidden", "FAIL", "%d forbidden token occurrence(s)" % len(hits), hits[:60])
        if len(hits) > 60:
            rep.detail("forbidden", "... %d more" % (len(hits) - 60))
    else:
        rep.set("forbidden", "PASS", "none of %d forbidden patterns occur (ground rule 1's words: anywhere; "
                "command words: outside comments and strings; comments never split a token)" % len(FORBIDDEN))

    # ---- (d) structure
    probs, fw_rels, req_lines = [], set(), []
    for (ln, why) in a.struct_errors:
        probs.append("line %d: %s" % (ln, why))
    if a.open_at_eof:
        probs.append("file ends inside %s" % ", ".join("%s %s" % kv for kv in a.open_at_eof))
    reqs, bad = parse_requires(a)
    for (ln, why) in bad:
        probs.append("line %d: %s" % (ln, why))
        dangerous.append("line %d: unparseable Require" % ln)
    for (ln, root, name) in reqs:
        kind, rels, why = classify_require(idx, root, name)
        shown = ("From %s " % root if root else "") + "Require " + name
        if kind == "reject":
            probs.append("line %d: %s" % (ln, why))
            dangerous.append("line %d: %s" % (ln, shown))
        elif kind == "framework":
            fw_rels.update(rels)
            req_lines.append("line %d: %s -> framework %s" % (ln, shown, ", ".join(rels)))
        else:
            req_lines.append("line %d: %s -> Coq stdlib" % (ln, shown))
    shadow_names = {"tm", "c0", "halts", "TM_from_str", thm}
    canon_tm, canon_thm = [], []
    for st in a.sentences:
        h = st.head
        kw = re.match(IDENT, h)
        kw = kw.group(0) if kw else ""
        if ROLLBACK_RE.search(st.prefix):
            probs.append("line %d: `%s` runs a command and rolls it back: never needed in a finished kill, and "
                         "it makes the text say something Coq does not keep" % (st.line, ROLLBACK_RE.search(st.prefix).group(0)))
            continue
        if kw in DANGEROUS_COMMANDS and re.match(re.escape(kw) + r"\b(?!\s*:=)", h):
            probs.append("line %d: %s" % (st.line, DANGEROUS_COMMANDS[kw]))
            dangerous.append("line %d: %s" % (st.line, kw))
        if re.match(r"(?:Variables?|Context)\b", h) and not st.in_section:
            probs.append("line %d: `%s` outside a Section declares a local axiom" % (st.line, kw))
        if re.match(r"(?:String|Number)\s+Notation\b", h):
            probs.append("line %d: `%s Notation` can change how literals are read" % (st.line, kw))
        if st.depth == 0 and re.match(r"Definition\s+tm(?![\w'])", h):
            canon_tm.append(st)
            continue
        if st.depth == 0 and re.match(r"(?:Lemma|Theorem|Corollary|Proposition|Fact|Remark|Example)\s+" +
                                      re.escape(thm) + r"(?![\w'])", h):
            canon_thm.append(st)
            continue
        for nm in shadow_hits(h, shadow_names):
            what = "defines a notation using `~`" if nm == "~" else "re-binds, re-declares or re-notates `%s`" % nm
            probs.append("line %d: %s (allowed: one top-level `Definition tm`, one top-level `%s`, and no "
                         "redefinition of c0/halts/TM_from_str/~)" % (st.line, what, thm))
    if a.trailing:
        probs.append("text after the last complete sentence: %r" % a.trailing[:60])
    if probs:
        rep.set("structure", "FAIL", "%d structural problem(s)" % len(probs), probs[:60])
    else:
        rep.set("structure", "PASS", "%d Require name(s) allowed; no top-level Variable/Context; no shadowing; "
                "Module/Section balanced" % len(reqs))
    for l in req_lines:
        rep.detail("structure", l)

    # ---- (b) TM literal (text)
    if len(canon_tm) != 1:
        rep.set("tm_text", "FAIL", "expected exactly one top-level `Definition tm`, found %d" % len(canon_tm),
                ["line %d" % st.line for st in canon_tm])
    else:
        st = canon_tm[0]
        lits = strings_in(a, st.start, st.end)
        if len(lits) != 1:
            rep.set("tm_text", "FAIL", "`Definition tm` (line %d) must contain exactly one string literal, has %d"
                    % (st.line, len(lits)))
        else:
            pre = a.code[st.start:lits[0][0]]
            lit = decode_literal(src, lits[0])
            if not re.search(r"\bTM_from_str\s*\(?\s*\Z", pre):
                rep.set("tm_text", "FAIL", "the literal in `Definition tm` (line %d) is not the argument of "
                        "TM_from_str" % st.line)
            elif lit.encode("utf-8") != tm.encode("utf-8"):
                rep.set("tm_text", "FAIL", "literal differs from <tm>", [
                    "file (line %d): %r" % (st.line, lit), "arg:            %r" % tm])
            else:
                rep.set("tm_text", "PASS", "line %d: TM_from_str \"%s\" == <tm> (%d bytes)" % (st.line, lit, len(tm)))
    for m in re.finditer(r"\bTM_from_str\b", a.code):
        if canon_tm and canon_tm[0].start <= m.start() < canon_tm[0].end:
            continue
        rest = a.code[m.end():]
        mm = re.match(r"\s*\(?\s*\"", rest)
        ln = line_of(a.line_starts, m.start())
        if mm:
            q = m.end() + mm.end() - 1
            k = skip_string(src, q)
            other = decode_literal(src, (q, k)) if k else "?"
            rep.warn("tm_text", "line %d: another TM_from_str literal %r%s" % (
                ln, other, "" if other == tm else " (a different machine)"))

    # ---- (c) theorem (text)
    want = {"nonhalt": {":~haltstmc0", ":~(haltstmc0)", ":not(haltstmc0)"}, "halt": {":haltstmc0"}}[mode]
    shown = "~halts tm c0" if mode == "nonhalt" else "halts tm c0"
    if len(canon_thm) != 1:
        rep.set("theorem_text", "FAIL", "expected exactly one top-level `Lemma/Theorem %s`, found %d"
                % (thm, len(canon_thm)), ["line %d" % st.line for st in canon_thm])
    else:
        st = canon_thm[0]
        m = re.match(r"\w+\s+" + re.escape(thm) + r"(?![\w'])(.*)\.\Z", st.head, re.S)
        stmt = re.sub(r"\s+", "", m.group(1)) if m else ""
        if stmt in want:
            rep.set("theorem_text", "PASS", "line %d: %s : %s" % (st.line, thm, shown))
        else:
            rep.set("theorem_text", "FAIL", "line %d: statement must read `%s : %s`, found `%s`" % (
                st.line, thm, shown, " ".join(m.group(1).split())[:120] if m else "?"))
    ctx["dangerous"] = dangerous
    ctx["fw_rels"] = sorted(fw_rels)


NATIVE_EXTS = (".cmxs", ".cmx", ".cmi")


def native_state(idx, rel):
    """'ok', 'missing' or 'stale' for the native code of framework file rel (its .vo exists).
    coqc -native-compiler yes writes it right after the .vo, next to it, as
    <dir>/.coq-native/N<logical path joined by `_`>.cmxs/.cmx/.cmi (verified on 8.20.1:
    TM.v -> .coq-native/NBusyCoq_TM.*, and Sub/A.v under `-Q . L` -> Sub/.coq-native/NL_Sub_A.*).
    The candidate's native code is compiled against the .cmi/.cmx and dynlinks the .cmxs. A
    BigInt/ file has two logical names (BusyCoq.BigInt.X, or BigInt.X from BigInt/Makefile);
    either name's files will do, since only the compile that wrote the .vo can leave files
    newer than it."""
    vo = os.path.join(VERIFY, rel[:-2] + ".vo")
    vo_mtime = os.path.getmtime(vo)
    state = "missing"
    for lp, r in idx:
        if r != rel:
            continue
        stem = os.path.join(os.path.dirname(vo), ".coq-native", "N" + "_".join(lp))
        if not all(os.path.exists(stem + e) for e in NATIVE_EXTS):
            continue
        if all(os.path.getmtime(stem + e) >= vo_mtime for e in NATIVE_EXTS):
            return "ok"
        state = "stale"
    return state


def check_framework_build(idx, start_rels, makefile_text, native):
    rels = framework_closure(idx, start_rels)
    missing, stale, native_bad = [], [], []
    for rel in rels:
        v = os.path.join(VERIFY, rel)
        vo = v[:-2] + ".vo"
        if not os.path.exists(vo):
            missing.append(rel)
        elif os.path.getmtime(vo) < os.path.getmtime(v):
            stale.append(rel)
        elif native != "no":
            ns = native_state(idx, rel)
            if ns != "ok":
                native_bad.append("%s (%s)" % (rel, ns))
    det = []
    if missing:
        not_in_make = [r for r in missing if os.path.basename(r) not in makefile_text]
        det.append("missing .vo for: " + ", ".join(missing[:20]) + (" ..." if len(missing) > 20 else ""))
        if not_in_make:
            det.append("not built by `make` (outside ALLVFILES), build explicitly: " + ", ".join(not_in_make[:10]))
    if stale:
        det.append(".vo older than its .v (rebuild): " + ", ".join(stale[:20]))
    if native_bad:
        det.append("-native-compiler %s needs each .vo's native code (.coq-native/N<name>%s) present and no older "
                   "than the .vo; missing or stale for: %s%s" % (native, "/".join(NATIVE_EXTS),
                                                              ", ".join(native_bad[:20]),
                                                              " ..." if len(native_bad) > 20 else ""))
    return rels, missing, stale, native_bad, det


# ======================================================================== Coq phase
def find_tool(env_name, exe):
    v = os.environ.get(env_name)
    if v:
        return shutil.which(v) or (v if os.path.isfile(v) and os.access(v, os.X_OK) else None)
    p = shutil.which(exe)
    if p:
        return p
    cands = sorted(glob.glob(os.path.expanduser("~/.opam/*/bin/" + exe)))
    pref = [c for c in cands if "/.opam/default/" in c]
    return (pref or cands or [None])[0]


def coqproject_flags():
    path = os.path.join(VERIFY, "_CoqProject")
    toks = shlex.split(open(path, encoding="utf-8").read(), comments=True)
    flags, native, i = [], None, 0
    while i < len(toks):
        t = toks[i]
        if t in ("-Q", "-R") and i + 2 < len(toks):
            flags += [t, os.path.normpath(os.path.join(VERIFY, toks[i + 1])), toks[i + 2]]
            i += 3
        elif t == "-I" and i + 1 < len(toks):
            flags += ["-I", os.path.normpath(os.path.join(VERIFY, toks[i + 1]))]
            i += 2
        elif t == "-native-compiler" and i + 1 < len(toks):
            native = toks[i + 1]
            i += 2
        elif t.endswith((".v", ".ml", ".mli", ".mlg", ".mllib", ".mlpack")) and not t.startswith("-"):
            i += 1
        else:
            raise RuntimeError("unexpected _CoqProject token %r: update check_kill.sh" % t)
    return flags, native


def coq_string_term(s, sp, ip):
    term = sp + ".Strings.String.EmptyString"
    for ch in reversed(s):
        b = ord(ch)
        bits = " ".join(ip + ".Init.Datatypes." + ("true" if (b >> k) & 1 else "false") for k in range(8))
        term = "(%s.Strings.String.String (%s.Strings.Ascii.Ascii %s) %s)" % (sp, sp, bits, term)
    return term


def statement(mode, fq, tm_term, ip):
    h = "(@%s %s %s)" % (fq["halts"], tm_term, fq["c0"])
    return ("(@%s.Init.Logic.not %s)" % (ip, h)) if mode == "nonhalt" else h


HEADER_RE = re.compile(r"([A-Z][A-Za-z ]*[A-Za-z]):\Z")


def parse_assumptions(text):
    """Parse Print Assumptions output (possibly several concatenated, '#' comment lines
    ignored) into a set of keys 'Section|<whole entry>', whitespace-normalised: for
    'name : type' entries the key holds the type too, so a baseline axiom never admits a
    different statement under the same name. Returns (keys, problems, saw_output)."""
    entries, problems = [], []
    section, cur, saw = None, None, False

    def flush():
        nonlocal cur
        if cur is not None:
            entries.append((section, " ".join(" ".join(cur).split())))
            cur = None

    for raw in text.splitlines():
        line = raw.rstrip()
        if not line.strip() or line.startswith("#"):
            flush()
            continue
        if line.strip() == "Closed under the global context":
            flush()
            section, saw = None, True
            continue
        if not line[0].isspace():
            flush()
            m = HEADER_RE.match(line)
            if m:
                section, saw = m.group(1), True
                continue
            if section is None:
                problems.append(line)
                continue
            cur = [line.strip()]
        else:
            if cur is None:
                problems.append(line.strip())
                continue
            cur.append(line.strip())
    flush()
    keys = {"%s|%s" % (sec, txt) for sec, txt in entries}
    for p in problems:
        keys.add("?|" + p)
    return keys, problems, saw


def entry_name(k):
    """The printed name an assumption key starts with (`Candidate.X.q0`, `Classical_Prop.classic`)."""
    return k.partition("|")[2].split(" ", 1)[0]


def basename_key(k):
    """'Section|base name' only: used for the in-file output, where names print relative to
    the candidate and types use its notations, so only a weak comparison is possible."""
    return "%s|%s" % (k.partition("|")[0], entry_name(k).split(".")[-1])


def between_markers(text, begin, end):
    """Output between the line containing `begin` and the line containing `end`. Markers carry
    a per-run nonce the candidate cannot know; each must occur exactly once. Return
    (body, None) or (None, problem)."""
    lines = text.splitlines()
    bi = [k for k, l in enumerate(lines) if begin in l]
    ei = [k for k, l in enumerate(lines) if end in l]
    if len(bi) != 1 or len(ei) != 1 or ei[0] < bi[0]:
        return None, "expected one %s line then one %s line in coqc output, found %d and %d" % (
            begin, end, len(bi), len(ei))
    body = lines[bi[0] + 1:ei[0]]
    while body and re.fullmatch(r"\s*:\s*\S.*", body[0]):  # the `: unit` line of `Check`
        body = body[1:]
    return "\n".join(body), None


def coqchk_own_entries(out, own_prefix):
    """'Section: name' for every name under coqchk -o's CONTEXT SUMMARY that starts with
    own_prefix (the candidate's library), or None if there is no summary."""
    if "CONTEXT SUMMARY" not in out:
        return None
    own, section = [], None
    for l in out.splitlines():
        m = re.match(r"\* (.+?):", l)
        if m:
            section = m.group(1)
        elif section and l[:1].isspace() and l.strip().startswith(own_prefix):
            own.append("%s: %s" % (section, l.strip()))
    return own


# Lines in which coqchk reports a failure (8.20: `Fatal Error: ...`, `Error: ...`, `Anomaly ...`).
COQCHK_ERROR_RE = re.compile(r"^(?:Error|Anomaly|Fatal)\b.*", re.M)


def parse_ml_modules(body):
    """Names listed by `Print ML Modules` (`ltac_plugin.cmxs (using legacy method)`,
    `coq-core.plugins.extraction`) -> (all names, names that are not stock proof plugins)."""
    names = [l.split()[0] for l in body.splitlines() if l.strip() and not l.startswith("Loaded ML Modules")]
    bad = []
    for n in names:
        m = re.fullmatch(r"(?:(?:coq-core|rocq-runtime)\.plugins\.)?([a-z0-9_]+?)(?:_plugin)?(?:\.cmxs|\.cma)?", n)
        if not m or m.group(1) not in STOCK_PLUGINS:
            bad.append(n)
    return names, bad


def first_error(stderr, fname):
    """Locate the first `Error` in coqc's stderr. Return (line or None, message, in_file) where
    in_file says whether the location printed just before it is in `fname` (it can also be a
    generated native-code file, or missing)."""
    lines = stderr.rstrip().splitlines()
    for k, l in enumerate(lines):
        if l.startswith("Error"):
            ln, in_file = None, False
            for j in range(k - 1, max(-1, k - 4), -1):
                m = re.match(r'File "([^"]*)", line (\d+), characters', lines[j])
                if m:
                    if os.path.basename(m.group(1)) == fname:
                        ln, in_file = int(m.group(2)), True
                    break
            return ln, " ".join(" ".join(lines[k:k + 12]).split())[:600], in_file
    return None, " ".join(" ".join(lines[-8:]).split())[:600], False


def coq_phase(rep, o, tm, shape, thm, mode, src_bytes, ctx):
    mod = SHAPES[shape]["module"]
    coqc = find_tool("COQC", "coqc")
    if not coqc:
        rep.set("coq", "FAIL", "coqc not found (set COQC=/path/to/coqc, or install Coq 8.20)")
        return
    # The environment of every coqc/coqchk run below, --version included.
    env = dict(os.environ)
    # coqc -native-compiler runs ocamlfind/ocamlopt from PATH; they must be the ones of
    # coqc's own installation (e.g. an opam switch not on PATH), or the OCaml versions clash.
    # Empty or relative entries would resolve against coqc's working directory (the temp
    # directory with the candidate's files), so only absolute ones are kept.
    bindir = os.path.dirname(os.path.realpath(coqc))
    inherited = [p for p in env.get("PATH", "").split(os.pathsep) if p and os.path.isabs(p) and p != bindir]
    env["PATH"] = os.pathsep.join([bindir] + inherited)
    for var in ("COQPATH", "ROCQPATH"):
        if env.pop(var, None) is not None:
            rep.warn("coq", "ignored $%s for the compile (load paths come from _CoqProject only)" % var)
    # Dropped rather than only warned about: OCAMLPARAM adds flags to every ocamlopt run (a
    # -ppx is arbitrary code, -unsafe drops bounds checks) and OCAMLFIND_* can swap the
    # toolchain or its config, so either could change the native code that decides
    # native_compute steps without anything in the report showing it. The verdict must not
    # depend on them; opam's environment never sets them. coqc and coqchk need neither (coqc
    # does read OCAMLFIND_* itself, to locate plugins: one more reason to drop them).
    for var in sorted(env):
        if var == "OCAMLPARAM" or var.startswith("OCAMLFIND_"):
            del env[var]
            rep.warn("coq", "ignored $%s (it would change how native code is compiled)" % var)
    if env.get("COQLIB"):
        rep.warn("coq", "$COQLIB is set (%s)" % env["COQLIB"])
    v = run_proc([coqc, "--version"], cwd=ROOT, timeout=120, env=env)
    m = re.search(r"version\s+(\d+)\.(\d+)(?:\.(\d+))?", v["out"] + v["err"])
    if v["rc"] != 0 or not m:
        rep.set("coq", "FAIL", "`%s --version` failed: %s" % (coqc, (v["out"] + v["err"]).strip()[:200]))
        return
    major, minor = int(m.group(1)), int(m.group(2))
    ver = ".".join(g for g in m.groups() if g)
    ip, sp = ("Corelib", "Stdlib") if major >= 9 else ("Coq", "Coq")
    ctx["coqc"], ctx["coqc_version"] = coqc, ver
    rep.set("coq", "PASS", "coqc %s (%s)" % (ver, coqc))
    if (major, minor) != (8, 20):
        rep.warn("coq", "busycoq is tested on Coq 8.20; this is %s" % ver)
    try:
        flags, _ = coqproject_flags()
    except (OSError, RuntimeError) as e:
        rep.set("compile", "FAIL", "cannot derive flags from verify/_CoqProject: %s" % e)
        return
    # Default `yes`, as in verify/_CoqProject (policy A): native_compute steps are then
    # checked by OCaml code generated and dynlinked at compile time, which Print Assumptions
    # never mentions -- the same trust upstream's accepted proofs rely on. `no` falls back to
    # the VM; Bouncer_v3 took 994 s that way vs 212 s native. parse_args
    # has already resolved $CHECK_KILL_NATIVE and validated the mode.
    native = o["native"]
    ctx["native"] = native
    if native != "no":
        rep.warn("compile", "-native-compiler %s: native code is in the trusted base unless coqchk finishes "
                 "(policy A)" % native)

    base = os.path.realpath(os.environ.get("CHECK_KILL_TMPDIR") or tempfile.gettempdir())
    if is_within(base, VENDOR):
        rep.set("compile", "FAIL", "temp base %s is inside vendor/; set CHECK_KILL_TMPDIR elsewhere" % base)
        return
    tmp = tempfile.mkdtemp(prefix="check_kill.", dir=base)
    ctx["tmp"] = tmp
    probe_dir, kill_dir = os.path.join(tmp, "probe"), os.path.join(tmp, "kill")
    os.mkdir(probe_dir)
    os.mkdir(kill_dir)

    # ---- names: resolve the framework's halts / c0 / TM_from_str to absolute names
    with open(os.path.join(probe_dir, "ProbeNames.v"), "w", encoding="utf-8") as f:
        f.write("From BusyCoq Require Import %s.\nLocate halts.\nLocate c0.\nLocate TM_from_str.\n" % mod)
    r = run_proc([coqc, "-q"] + flags + ["-Q", probe_dir, PROBE_LIB, "-native-compiler", "no", "ProbeNames.v"],
                 cwd=probe_dir, timeout=600, env=env)
    exp = expected_fqns(mod)
    fq = {}
    for nm in ("halts", "c0", "TM_from_str"):
        mm = re.search(r"^Constant\s+(BusyCoq\.%s\.(?:\S+\.)?%s)\s*$" % (re.escape(mod), re.escape(nm)),
                       r["out"], re.M)
        if mm:
            fq[nm] = mm.group(1)
    if r["rc"] != 0 or len(fq) != 3:
        msg = first_error(r["err"], "ProbeNames.v")[1] if r["rc"] != 0 else "Locate output: " + " | ".join(tail(r["out"], 8))
        hint = ""
        if "Cannot find" in r["err"] or "not found" in r["err"] or "Unable to locate" in r["err"]:
            hint = " -- build the framework first: (cd vendor/busycoq/verify && make)"
        rep.set("names", "FAIL", "could not resolve framework names: " + msg + hint)
        return
    ctx["fqns"] = fq
    rep.set("names", "PASS", "halts, c0, TM_from_str resolved inside %s" % mod,
            ["%s = %s" % (k, fq[k]) for k in ("halts", "c0", "TM_from_str")])
    for k in fq:
        if fq[k] != exp[k]:
            rep.warn("names", "%s resolved to %s, expected %s from reading the sources" % (k, fq[k], exp[k]))

    # ---- candidate: exact copy of the input + appended checks
    K = LIB + "." + CAND
    lit_term = coq_string_term(tm, sp, ip)
    # Output markers carry a per-run nonce: the candidate can print the text "CHECK_KILL__..."
    # (by computing the string), but not a nonce drawn after it was written.
    nonce = secrets.token_hex(8)

    def mark(tag):
        return "CHECK_KILL__%s_%s" % (tag, nonce)

    def mark_def(tag):
        return "Definition %s : %s.Init.Datatypes.unit := %s.Init.Datatypes.tt." % (mark(tag), ip, ip)

    block = [
        ("(* ===== check_kill.sh appended checks (temp copy only; the original is never edited) ===== *)", "hdr"),
        (mark_def("BEGIN"), "marker"),
        (mark_def("END"), "marker"),
        ("Check %s.%s." % (K, mark("BEGIN")), "marker"),
        ("Print Assumptions %s.%s." % (K, thm), "assume"),
        ("Check %s.%s." % (K, mark("END")), "marker"),
        ("Definition CHECK_KILL__stmt_tm : %s := %s.%s." % (statement(mode, fq, K + ".tm", ip), K, thm), "stmt_tm"),
        ("Definition CHECK_KILL__lit : %s.Strings.String.string := %s." % (sp, lit_term), "lit"),
        ("Definition CHECK_KILL__tm_conv : @%s.Init.Logic.eq _ %s.tm (@%s %s.CHECK_KILL__lit) := "
         "@%s.Init.Logic.eq_refl _ %s.tm." % (ip, K, fq["TM_from_str"], K, ip, K), "tm_conv"),
        ("Definition CHECK_KILL__stmt_lit : %s := %s.%s." % (
            statement(mode, fq, "(@%s %s.CHECK_KILL__lit)" % (fq["TM_from_str"], K), ip), K, thm), "stmt_lit"),
    ]
    prefix = src_bytes if src_bytes.endswith(b"\n") else src_bytes + b"\n"
    first_block_line = prefix.count(b"\n") + 1
    with open(os.path.join(kill_dir, CAND + ".v"), "wb") as f:
        f.write(prefix + ("\n".join(t for t, _ in block) + "\n").encode("utf-8"))
    cmd = [coqc, "-q"] + flags + ["-Q", kill_dir, LIB, "-native-compiler", native, CAND + ".v"]
    ctx["coqc_cmd"] = " ".join(shlex.quote(x) for x in cmd)
    print("check_kill: compiling temp copy (timeout %ds, -native-compiler %s) ..." % (o["timeout"], native),
          file=sys.stderr, flush=True)
    r = run_proc(cmd, cwd=kill_dir, timeout=o["timeout"], env=env)
    ctx["compile_seconds"] = r["seconds"]
    rep.detail("compile", "command: " + ctx["coqc_cmd"])
    rep.detail("compile", "wall time: %.1fs" % r["seconds"])
    infile = {"stmt_tm": None, "tm_conv": None, "stmt_lit": None, "assume": None}
    order = ["assume", "stmt_tm", "tm_conv", "stmt_lit"]
    if r["timed_out"]:
        rep.set("compile", "FAIL", "timed out after %ds" % o["timeout"])
        return
    if r["rc"] != 0:
        ln, msg, _ = first_error(r["err"], CAND + ".v")
        if ln is None or ln < first_block_line:
            where = ("line %d" % ln) if ln else "after the last sentence or outside the file"
            rep.set("compile", "FAIL", "the file does not compile (%s): %s" % (where, msg),
                    ["stderr tail:"] + ["  " + l for l in tail(r["err"], 20)])
            if native == "yes" and ("native" in r["err"].lower() or "ocamlfind" in r["err"]):
                rep.detail("compile", "hint: native compilation problem; retry with --native no to confirm")
            return
        tag = block[ln - first_block_line][1] if ln - first_block_line < len(block) else "?"
        rep.set("compile", "PASS", "the file itself compiles; an appended check failed (%s, line %d)" % (tag, ln))
        failed_tag = {"marker": "assume", "hdr": "assume", "lit": "tm_conv"}.get(tag, tag)
        for t in order:
            if t == failed_tag:
                infile[t] = msg
                break
            infile[t] = True
    else:
        rep.set("compile", "PASS", "compiled in %.1fs with all appended checks" % r["seconds"])
        for t in order:
            infile[t] = True
    seen = {}
    for l in r["err"].splitlines():
        if l.startswith("Warning"):
            seen[l[:160]] = seen.get(l[:160], 0) + 1
    for k, (l, n) in enumerate(seen.items()):
        if k == 8:
            rep.warn("compile", "... %d more distinct warnings" % (len(seen) - 8))
            break
        rep.warn("compile", l + (" (x%d)" % n if n > 1 else ""))
    infile_assum = None
    if infile["assume"] is True:
        infile_assum, why = between_markers(r["out"], mark("BEGIN"), mark("END"))
        if why:
            infile["assume"] = "in-file Print Assumptions: " + why

    # ---- isolated checker: Require (never Import) the compiled copy, re-state everything
    iso = {"isolation": None, "tm_conv": None, "stmt_tm": None, "stmt_lit": None, "assume": None}
    iso_assum = None
    vo = os.path.join(kill_dir, CAND + ".vo")
    if r["rc"] == 0 and os.path.exists(vo):
        C = LIB + "." + CHECKER
        lines = [
            ("(* check_kill.sh isolated checker: the candidate is Required, never Imported, so none of its", "load"),
            ("   notations, scopes or short names are in effect here. Its #[global] options DO survive", "load"),
            ("   Require, so every option that matters is put back after it, and the result is printed. *)", "load"),
            ("Require BusyCoq.%s." % mod, "load"),
            ("Require %s.Strings.String %s.Strings.Ascii." % (sp, sp), "load"),
            ("Require %s." % K, "load"),
            ("Set Guard Checking.", "load"),
            ("Set Positivity Checking.", "load"),
            ("Set Universe Checking.", "load"),
            ("Unset Definitional UIP.", "load"),
            ("Unset Program Mode.", "load"),
            ("Unset Printing All.", "load"),
        ] + [(mark_def(t), "load") for t in ("ML_BEGIN", "ML_END", "FLAGS_BEGIN", "FLAGS_END", "ISO_BEGIN", "ISO_END")] + [
            ("Check %s.%s." % (C, mark("ML_BEGIN")), "isolation"),
            ("Print ML Modules.", "isolation"),
            ("Check %s.%s." % (C, mark("ML_END")), "isolation"),
            ("Check %s.%s." % (C, mark("FLAGS_BEGIN")), "isolation"),
            ("Print Typing Flags.", "isolation"),
            ("Check %s.%s." % (C, mark("FLAGS_END")), "isolation"),
            ("Definition lit : %s.Strings.String.string := %s." % (sp, lit_term), "tm_conv"),
            ("Definition tm_conv : @%s.Init.Logic.eq _ %s.tm (@%s %s.lit) := @%s.Init.Logic.eq_refl _ %s.tm."
             % (ip, K, fq["TM_from_str"], C, ip, K), "tm_conv"),
            ("Definition stmt_tm : %s := %s.%s." % (statement(mode, fq, K + ".tm", ip), K, thm), "stmt_tm"),
            ("Definition stmt_lit : %s := %s.%s." % (
                statement(mode, fq, "(@%s %s.lit)" % (fq["TM_from_str"], C), ip), K, thm), "stmt_lit"),
            ("Check %s.%s." % (C, mark("ISO_BEGIN")), "assume"),
            ("Print Assumptions %s.stmt_lit." % C, "assume"),
            ("Check %s.%s." % (C, mark("ISO_END")), "assume"),
        ]
        with open(os.path.join(kill_dir, CHECKER + ".v"), "w", encoding="utf-8") as f:
            f.write("\n".join(t for t, _ in lines) + "\n")
        r2 = run_proc([coqc, "-q"] + flags + ["-Q", kill_dir, LIB, "-native-compiler", "no", CHECKER + ".v"],
                      cwd=kill_dir, timeout=max(600, o["timeout"]), env=env)
        iso_order = ["load", "isolation", "tm_conv", "stmt_tm", "stmt_lit", "assume"]
        if r2["rc"] == 0:
            for t in iso_order[1:]:
                iso[t] = True
        else:
            ln, msg, _ = first_error(r2["err"], CHECKER + ".v")
            msg = "timed out" if r2["timed_out"] else msg
            tag = lines[ln - 1][1] if ln and ln <= len(lines) else "load"
            for t in iso_order:
                if t == tag:
                    if t == "load":
                        for u in iso_order[1:]:
                            iso[u] = "isolated checker could not load the candidate: " + msg
                    else:
                        iso[t] = msg
                    break
                if t != "load":
                    iso[t] = True
        if iso["isolation"] is True:   # (g) what the candidate's Require left behind
            probs = []
            ml, why = between_markers(r2["out"], mark("ML_BEGIN"), mark("ML_END"))
            if why:
                probs.append("Print ML Modules: " + why)
            else:
                names, bad = parse_ml_modules(ml)
                ctx["ml_modules"] = names
                if not names:
                    probs.append("Print ML Modules output not understood: %r" % ml[:200])
                if bad:
                    probs.append("ML plugin(s) other than the stock proof plugins are loaded: " + ", ".join(bad))
            fl, why = between_markers(r2["out"], mark("FLAGS_BEGIN"), mark("FLAGS_END"))
            if why:
                probs.append("Print Typing Flags: " + why)
            else:
                got = [l.strip() for l in fl.splitlines() if l.strip()]
                if got != EXPECTED_TYPING_FLAGS:
                    probs.append("typing flags read `%s`, expected `%s`" % ("; ".join(got), "; ".join(EXPECTED_TYPING_FLAGS)))
            iso["isolation"] = "; ".join(probs) if probs else True
        if iso["assume"] is True:
            iso_assum, why = between_markers(r2["out"], mark("ISO_BEGIN"), mark("ISO_END"))
            if why:
                iso["assume"] = "isolated Print Assumptions: " + why
    else:
        for t in iso:
            iso[t] = "not run (the temp copy did not finish compiling)"

    def verdict(cid, parts, ok_summary):
        bad = [(name, val) for name, val in parts if val is not True]
        if not bad:
            rep.set(cid, "PASS", ok_summary, ["%s: ok" % name for name, _ in parts])
        else:
            rep.set(cid, "FAIL", "; ".join("%s: %s" % (n, "not reached" if v is None else v) for n, v in bad)[:900],
                    ["%s: %s" % (n, "ok" if v is True else ("not reached" if v is None else "FAILED")) for n, v in parts])

    stmt_txt = ("~ halts" if mode == "nonhalt" else "halts")
    verdict("tm_rocq", [("in-file tm_conv", infile["tm_conv"]), ("isolated tm_conv", iso["tm_conv"])],
            "%s.tm = %s \"%s\" by eq_refl (in-file and isolated)" % (K, fq["TM_from_str"], tm))
    verdict("theorem_rocq", [("in-file %s : %s tm c0" % (thm, stmt_txt), infile["stmt_tm"]),
                             ("in-file %s : %s (TM_from_str lit) c0" % (thm, stmt_txt), infile["stmt_lit"]),
                             ("isolated %s : %s tm c0" % (thm, stmt_txt), iso["stmt_tm"]),
                             ("isolated %s : %s (TM_from_str lit) c0" % (thm, stmt_txt), iso["stmt_lit"])],
            "%s : %s (TM_from_str \"%s\") c0 with absolute names (in-file and isolated)" % (thm, stmt_txt, tm))
    verdict("isolation", [("isolated checker plugins and typing flags", iso["isolation"])],
            "only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off")
    if ctx.get("ml_modules"):
        rep.detail("isolation", "ML modules: " + ", ".join(ctx["ml_modules"]))

    # ---- (e) assumptions
    ctx["assumptions_raw"] = iso_assum
    if infile["assume"] is not True or iso["assume"] is not True or iso_assum is None:
        why = []
        if infile["assume"] is not True:
            why.append("in-file: " + ("not reached" if infile["assume"] is None else str(infile["assume"])))
        if iso["assume"] is not True:
            why.append("isolated: " + ("not reached" if iso["assume"] is None else str(iso["assume"])))
        rep.set("assumptions", "FAIL", "Print Assumptions not obtained: " + "; ".join(why)[:600])
    else:
        iso_keys, iso_probs, iso_saw = parse_assumptions(iso_assum)
        in_keys, in_probs, in_saw = parse_assumptions(infile_assum or "")
        ctx["assumptions"] = sorted(iso_keys)
        det = ["isolated Print Assumptions (%d): %s" % (len(iso_keys), ", ".join(sorted(iso_keys)) or "closed")]
        problems = []
        if not iso_saw or iso_probs:
            problems.append("isolated output not understood: %r" % iso_assum[:300])
        if not in_saw or in_probs:
            problems.append("in-file output not understood: %r" % (infile_assum or "")[:300])
        # failures whatever the baseline says (and never recordable into it)
        unsafe = sorted(k for k in iso_keys | in_keys if UNSAFE_ENTRY_RE.search(k))
        own = sorted(k for k in iso_keys if OWN_NAME_RE.match(entry_name(k)) and k not in unsafe)
        if unsafe:
            problems.append("kernel checks were switched off: " + ", ".join(unsafe))
        if own:
            problems.append("assumptions declared by the file itself: " + ", ".join(own))
        if o["emit"]:
            try:
                with open(o["emit"], "w", encoding="utf-8") as f:
                    f.write(iso_assum.rstrip("\n") + "\n")
                det.append("raw isolated output written to " + o["emit"])
            except OSError as e:
                problems.append("cannot write %s: %s" % (o["emit"], e))
            if problems:
                rep.set("assumptions", "FAIL", "; ".join(problems), det)
            else:
                rep.set("assumptions", "SKIP", "baseline comparison skipped (--emit-assumptions)", det)
        elif not os.path.isfile(BASELINE_FILE):
            rep.set("assumptions", "FAIL", "tools/assumptions_baseline.txt is missing: run tools/make_baseline.sh "
                    "(after the framework is built) and review it", det)
        else:
            base_text = open(BASELINE_FILE, encoding="utf-8", errors="replace").read()
            base_keys, base_probs, base_saw = parse_assumptions(base_text)
            untrustable = [k for k in base_keys if UNSAFE_ENTRY_RE.search(k) or OWN_NAME_RE.match(entry_name(k))]
            if base_probs or not base_saw or untrustable:
                problems.append("baseline file invalid (not understood: %s; entries that can never be trusted: %s)"
                                % (base_probs[:5], untrustable[:5]))
            # authoritative: whole entries (name AND type) of the isolated checker's output
            extra = sorted(iso_keys - base_keys - set(unsafe) - set(own))
            # cross-check only: the in-file output prints names relative to the candidate and
            # types with its notations, so it can be compared by base name only
            extra_in = sorted({basename_key(k) for k in in_keys} - {basename_key(k) for k in base_keys})
            if extra:
                problems.append("isolated: not in baseline: " + ", ".join(extra))
            if extra_in:
                problems.append("in-file (by base name): not in baseline: " + ", ".join(extra_in))
            det.append("baseline entries (%d): %s" % (len(base_keys), ", ".join(sorted(base_keys)) or "closed"))
            if problems:
                rep.set("assumptions", "FAIL", "; ".join(problems)[:900], det)
            else:
                rep.set("assumptions", "PASS", "%d assumption(s), all in the baseline" % len(iso_keys), det)

    # ---- (h) coqchk: an independent kernel re-checks the compiled candidate (on by default)
    if o["coqchk"]:
        coqchk = find_tool("COQCHK", "coqchk")
        if not coqchk:
            ctx["coqchk_outcome"] = "fail"
            rep.set("coqchk", "FAIL", "coqchk not found")
        elif r["rc"] != 0:
            ctx["coqchk_outcome"] = "fail"
            rep.set("coqchk", "FAIL", "not run: the temp copy did not compile")
        else:
            qflags = []
            i = 0
            while i < len(flags):
                if flags[i] in ("-Q", "-R"):
                    qflags += flags[i:i + 3]
                    i += 3
                else:
                    i += 1
            # -o prints a CONTEXT SUMMARY of every loaded library: axioms, constants relying on
            # unsafe fixpoints / type-in-type, inductives with assumed positivity. coqchk itself
            # accepts constants whose checks were switched off (it honours their typing flags),
            # so the summary is what makes it a second, independent reporter: nothing in it may
            # belong to the candidate. (Definitional UIP does not appear there; (e) covers it.)
            r3 = run_proc([coqchk, "-silent", "-o"] + qflags + ["-Q", kill_dir, LIB, "-norec", K], cwd=kill_dir,
                          timeout=o["coqchk_timeout"], env=env)
            ctx["coqchk_seconds"] = r3["seconds"]
            both = r3["out"] + "\n" + r3["err"]
            own = coqchk_own_entries(both, LIB + ".")   # 8.20 prints it on stderr
            if r3["timed_out"]:
                # Policy A: coqchk re-does native/VM steps by plain conversion, which can take
                # hours (Bouncer_v3: >80 min vs 212 s to compile). A timeout is advisory only
                # (the verdict code lets exactly this SKIP through), but what coqchk printed
                # before it was stopped still counts: an error or a finding there is a FAIL.
                found = COQCHK_ERROR_RE.findall(both) + (own or [])
                if found:
                    ctx["coqchk_outcome"] = "fail"
                    rep.set("coqchk", "FAIL", ("timed out after %ds, and its partial output already reports: %s"
                                               % (o["coqchk_timeout"], " | ".join(found)))[:900])
                else:
                    ctx["coqchk_outcome"] = "timeout"
                    rep.set("coqchk", "SKIP", "timed out after %ds (advisory under policy A; not a failure)"
                            % o["coqchk_timeout"])
                    rep.warn("coqchk", "coqchk did not finish: the kill rests on coqc's kernel check at Qed")
            elif r3["rc"] != 0:
                ctx["coqchk_outcome"] = "fail"
                rep.set("coqchk", "FAIL", "coqchk failed: " + first_error(r3["err"] + r3["out"], "")[1])
            elif own is None:
                ctx["coqchk_outcome"] = "fail"
                rep.set("coqchk", "FAIL", "coqchk -o printed no CONTEXT SUMMARY: " +
                        " | ".join(tail(both, 6)))
            elif own:
                ctx["coqchk_outcome"] = "fail"
                rep.set("coqchk", "FAIL", "coqchk lists assumptions of the file itself: " + ", ".join(own)[:600])
            else:
                ctx["coqchk_outcome"] = "pass"
                rep.set("coqchk", "PASS", "coqchk -norec %s ok (%.1fs); its context summary lists nothing of the "
                        "file's own" % (K, r3["seconds"]))


# ======================================================================== main
def parse_args(args):
    o = {"halt": False, "name": None, "timeout": 1800, "coqchk_timeout": 600, "json": False, "text_only": False, "keep": False,
         "emit": None, "selftest": False, "coqchk": True, "native": None, "help": False}
    pos, i = [], 0

    def need(k):
        if k + 1 >= len(args):
            raise UsageError("%s needs a value" % args[k])
        return args[k + 1]

    while i < len(args):
        a = args[i]
        if a == "--":
            pos += args[i + 1:]
            break
        if a in ("-h", "--help"):
            o["help"] = True
        elif a == "--halt":
            o["halt"] = True
        elif a == "--json":
            o["json"] = True
        elif a == "--text-only":
            o["text_only"] = True
        elif a == "--keep":
            o["keep"] = True
        elif a == "--selftest":
            o["selftest"] = True
        elif a == "--coqchk":
            o["coqchk"] = True
        elif a == "--no-coqchk":
            o["coqchk"] = False
        elif a in ("--timeout", "--coqchk-timeout", "--name", "--native", "--emit-assumptions") or \
                a.split("=", 1)[0] in ("--timeout", "--coqchk-timeout", "--name", "--native", "--emit-assumptions"):
            key, val = (a.split("=", 1) if "=" in a else (a, need(i)))
            if "=" not in a:
                i += 1
            if key in ("--timeout", "--coqchk-timeout"):
                # length first: int() refuses strings of more than 4300 digits (ValueError)
                if (not re.fullmatch(r"[1-9][0-9]*", val) or len(val) > len(str(MAX_TIMEOUT))
                        or int(val) > MAX_TIMEOUT):
                    raise UsageError("%s needs a positive integer of at most %d (one week)" % (key, MAX_TIMEOUT))
                o["timeout" if key == "--timeout" else "coqchk_timeout"] = int(val)
            elif key == "--name":
                if not re.fullmatch(IDENT, val):
                    raise UsageError("--name needs an identifier")
                o["name"] = val
            elif key == "--native":
                if val not in NATIVE_MODES:
                    raise UsageError("--native must be yes, no or ondemand")
                o["native"] = val
            else:
                o["emit"] = os.path.abspath(val)
        elif a.startswith("-") and len(a) > 1:
            raise UsageError("unknown option " + a)
        else:
            pos.append(a)
        i += 1
    if o["help"]:
        return o, pos
    if len(pos) != 2:
        raise UsageError("expected exactly two arguments: <file.v> <tm>")
    if o["text_only"] and (o["emit"] or o["selftest"]):
        raise UsageError("--text-only cannot be combined with --emit-assumptions/--selftest")
    if o["emit"] and o["selftest"]:
        raise UsageError("--emit-assumptions and --selftest are exclusive")
    if o["native"] is None:   # default: $CHECK_KILL_NATIVE, else yes as in verify/_CoqProject
        o["native"] = os.environ.get("CHECK_KILL_NATIVE") or "yes"
        if o["native"] not in NATIVE_MODES:
            raise UsageError("$CHECK_KILL_NATIVE must be yes, no or ondemand")
    return o, pos


def render(rep, o, result, exitc, ctx):
    out = []
    m = rep.meta
    out.append("check_kill %s" % m.get("file"))
    out.append("  tm %s | mode %s | theorem `%s` | sha256 %s" % (m.get("tm"), m.get("mode"), m.get("theorem"),
                                                                 (m.get("sha256") or "?")[:16]))
    out.append("-" * 78)
    for cid in rep.order:
        c = rep.checks[cid]
        out.append("[%s] %-14s %s" % (c["status"], cid, c["title"]))
        out.append("       %s" % c["summary"])
        for d in c["details"]:
            out.append("         %s" % d)
        for w in c["warnings"]:
            out.append("         warning: %s" % w)
    out.append("-" * 78)
    failed = rep.failed()
    note = {"PASS": "this is a kill", "TEXT_ONLY_OK": "text-level checks only; NOT a kill verdict",
            "SELFTEST_OK": "self-test mode; NOT a kill verdict",
            "BASELINE_SKIPPED": "baseline check skipped (--emit-assumptions); NOT a kill verdict"}.get(result, "")
    if result == "PASS" and ctx.get("coqchk_outcome") == "timeout":   # policy A: say what was not re-checked
        note = "this is a kill (coqchk did not finish within %ds: kernel check at Qed only; %s trusted)" % (
            o["coqchk_timeout"], "VM" if ctx.get("native") == "no" else "VM/native")
    elif result == "PASS" and not o["coqchk"]:
        note = "this is a kill (coqchk skipped by --no-coqchk: kernel check at Qed only)"
    if failed:
        note = "failed: " + ", ".join(failed)
    elif result == "FAIL":
        note = "incomplete: required checks were skipped (%s)" % ", ".join(
            c for c in rep.order if rep.checks[c]["status"] == "SKIP")
    out.append("RESULT: %s%s" % (result, (" -- " + note) if note else ""))
    if ctx.get("tmp") and o.get("keep"):
        out.append("temp dir kept: %s" % ctx["tmp"])
    return "\n".join(out)


def _exit_on_signal(signum, frame):
    # SystemExit unwinds normally: run_proc kills coqc's process group and main's `finally`
    # removes the temp dir. 128+N is never 0, so an interrupted run is never a kill.
    sys.exit(128 + signum)


def main():
    for s in (signal.SIGTERM, signal.SIGHUP):
        signal.signal(s, _exit_on_signal)
    try:
        o, pos = parse_args(ARGS)
    except UsageError as e:
        print("check_kill: %s\n%s" % (e, USAGE), file=sys.stderr)
        return 2
    if o["help"]:
        print(USAGE)
        return 2   # exit 0 is reserved for a kill
    file_arg, tm = pos
    mode = "halt" if o["halt"] else "nonhalt"
    thm = o["name"] or mode
    rep = Report()
    stmt = "~halts tm c0" if mode == "nonhalt" else "halts tm c0"
    for cid, title in [
        ("args", "arguments: TM string format and mode"),
        ("input", "input file: readable UTF-8 .v outside vendor/, lexically complete"),
        ("framework", "(a) busycoq HEAD == tools/busycoq.pin, no tracked changes under verify/"),
        ("framework_build", "(a) every framework .vo the file needs is built and newer than its .v%s" % (
            "" if o["native"] == "no" else ", with its native code")),
        ("forbidden", "(d) forbidden tokens anywhere in the file (comments and strings included)"),
        ("structure", "(d) Require allowlist, no top-level Variable/Context, no shadowing, balanced modules"),
        ("tm_text", "(b) TM_from_str literal of the top-level `Definition tm` == <tm> byte for byte"),
        ("theorem_text", "(c) exactly one top-level `%s : %s` (text)" % (thm, stmt)),
        ("coq", "Coq toolchain"),
        ("names", "absolute names of the framework's halts / c0 / TM_from_str (probe)"),
        ("compile", "(f) temp copy + appended checks compile within %ds, flags from verify/_CoqProject" % o["timeout"]),
        ("tm_rocq", "(b) Rocq: tm = TM_from_str \"<tm>\" by eq_refl (in-file + isolated checker)"),
        ("theorem_rocq", "(c) Rocq: %s : %s with absolute names (in-file + isolated checker)" % (thm, stmt)),
        ("isolation", "(g) isolated checker: stock proof plugins only; kernel checks on, definitional UIP off"),
        ("assumptions", "(e) Print Assumptions %s within tools/assumptions_baseline.txt" % thm),
    ] + ([("coqchk", "(h) coqchk -norec re-checks the compiled candidate (VM/native steps included)")]
         if o["coqchk"] else []) + [
        ("integrity", "input file and framework unchanged during the run"),
    ]:
        rep.add(cid, title)
    ctx = {"coqchk_outcome": "not_run"}   # coq_phase overrides it once check (h) is reached
    path = os.path.abspath(file_arg)
    rep.meta.update({"file": path, "tm": tm, "mode": mode, "theorem": thm})

    # ---- args
    shape, probs, warns = check_tm_format(tm)
    if probs:
        rep.set("args", "FAIL", "; ".join(probs))
    else:
        rep.set("args", "PASS", "%dx%d machine, framework module %s, mode %s" % (
            shape[0], shape[1], SHAPES[shape]["module"], mode))
        if shape != (6, 2):
            rep.warn("args", "not a BB(6) shape: fine for testing the oracle, not a BB(6) kill")
    for w in warns:
        rep.warn("args", w)

    # ---- input
    src_bytes, src = None, None
    real = os.path.realpath(path)
    if not os.path.isfile(real):
        rep.set("input", "FAIL", "no such file: %s" % path)
    elif not real.endswith(".v"):
        rep.set("input", "FAIL", "the file must have a .v extension")
    elif is_within(real, VENDOR):
        rep.set("input", "FAIL", "the file is inside vendor/; kills live in machines/<tm>/ (copy it out to test)")
    else:
        try:
            with open(real, "rb") as f:
                src_bytes = f.read()
            src = src_bytes.decode("utf-8")
        except (OSError, UnicodeDecodeError) as e:
            rep.set("input", "FAIL", "cannot read as UTF-8: %s" % e)
            src = None
    a = None
    if src is not None:
        rep.meta["sha256"] = sha256_bytes(src_bytes)
        if src.startswith(""):
            # Coq skips a leading UTF-8 BOM; analyse a space in its place so offsets stay put
            # (the temp copy that coqc compiles keeps the original bytes).
            src = " " + src[1:]
            rep.warn("input", "the file starts with a UTF-8 byte-order mark (Coq ignores it)")
        probs = []
        if "\0" in src:
            probs.append("NUL byte in file")
        bidi = [c for c in src if c in "‪‫‬‭‮⁦⁧⁨⁩‎‏"]
        if bidi:
            probs.append("%d bidirectional-control character(s): the text a reviewer sees may differ from "
                         "what Coq reads" % len(bidi))
        hidden = [c for c in src if c in "​‌‍⁠"]
        if hidden:
            probs.append("%d zero-width character(s) (or a byte-order mark after the start): the text a "
                         "reviewer sees may differ from what Coq reads" % len(hidden))
        a = analyze(src)
        for (why, pos_) in a.lex_errors:
            probs.append("%s at line %d" % (why, line_of(a.line_starts, pos_)))
        if probs:
            rep.set("input", "FAIL", "; ".join(probs))
        else:
            nonascii = sum(1 for c in src if ord(c) > 127)
            rep.set("input", "PASS", "%d bytes, %d lines, %d sentences%s" % (
                len(src_bytes), src.count("\n"), len(a.sentences),
                (", %d non-ASCII chars" % nonascii) if nonascii else ""))

    # ---- (a) framework
    fw = framework_state()
    rep.meta["framework_head"] = fw.get("head")
    if fw["ok"]:
        rep.set("framework", "PASS", "HEAD %s == pin; no tracked changes under verify/" % fw["head"])
    else:
        rep.set("framework", "FAIL", "; ".join(fw["problems"]))
    untracked_v = [u for u in fw["untracked"] if u.endswith(".v")]
    if untracked_v:
        rep.warn("framework", "untracked .v under verify/ (never Required by a kill): " + ", ".join(untracked_v[:10]))
    idx = build_index(fw["tracked_v"])

    # ---- (d)(b)(c) text checks
    if a is not None:
        run_text_checks(rep, a, tm, thm, mode, idx, ctx)
    else:
        for cid in ("forbidden", "structure", "tm_text", "theorem_text"):
            rep.set(cid, "FAIL", "not run: input unreadable")
        ctx["dangerous"] = ["input unreadable"]

    # ---- (a) framework build
    if shape and fw["tracked_v"]:
        start = ["%s.v" % SHAPES[shape]["module"]] + ctx.get("fw_rels", [])
        try:
            mk = open(os.path.join(VERIFY, "Makefile"), encoding="utf-8", errors="replace").read()
        except OSError:
            mk = ""
        rels, missing, stale, native_bad, det = check_framework_build(idx, start, mk, o["native"])
        if missing or stale or native_bad:
            status = "SKIP" if o["text_only"] else "FAIL"
            summary = ("%d of %d needed .vo missing, %d stale" % (len(missing), len(rels), len(stale)))
            if native_bad:
                summary += ", %d without fresh native code" % len(native_bad)
            summary += (" (dry run: build later)" if o["text_only"] else
                        " -- rebuild the framework: (cd vendor/busycoq/verify && make)")
            rep.set("framework_build", status, summary, det)
        else:
            rep.set("framework_build", "PASS", "%d needed framework .vo files present and fresh%s" % (
                len(rels), "" if o["native"] == "no" else ", with native code no older than the .vo"))
    else:
        rep.set("framework_build", "FAIL", "not run: bad TM string or framework not readable")

    # ---- Coq phase
    text_ids = ("args", "input", "forbidden", "structure", "tm_text", "theorem_text")
    text_ok = all(rep.status(c) == "PASS" for c in text_ids)
    fw_ok = rep.status("framework") == "PASS" and rep.status("framework_build") == "PASS"
    coq_ids = (["coq", "names", "compile", "tm_rocq", "theorem_rocq", "isolation", "assumptions"] +
               (["coqchk"] if o["coqchk"] else []))
    if not o["coqchk"] and not o["text_only"]:
        rep.warn("compile", "coqchk skipped (--no-coqchk): VM and native results get no second check")
    reason = None
    if o["text_only"]:
        reason = "dry run (--text-only)"
    elif rep.status("args") != "PASS" or rep.status("input") != "PASS":
        reason = "bad arguments or unreadable input"
    elif ctx.get("dangerous"):
        reason = "refusing to run coqc: dangerous content (%s)" % "; ".join(ctx["dangerous"][:5])
    elif not fw_ok:
        reason = "framework check failed"
    elif not text_ok and not o["selftest"]:
        reason = "text-level checks failed (--selftest compiles anyway, for testing the Rocq layers)"
    if reason:
        ctx["coqchk_outcome"] = "not_run"
        for cid in coq_ids:
            rep.set(cid, "SKIP", "not run: " + reason)
    else:
        try:
            coq_phase(rep, o, tm, shape, thm, mode, src_bytes, ctx)
        except Exception as e:  # internal error: report, never PASS
            for cid in coq_ids:
                if rep.status(cid) == "SKIP":
                    rep.set(cid, "FAIL", "internal error: %s: %s" % (type(e).__name__, e))
                    if cid == "coqchk":
                        ctx["coqchk_outcome"] = "fail"
        finally:
            if ctx.get("tmp") and not o["keep"]:
                shutil.rmtree(ctx["tmp"], ignore_errors=True)

    # ---- integrity
    if src_bytes is not None:
        try:
            now = open(real, "rb").read()
        except OSError:
            now = None
        fw2 = framework_state()
        probs = []
        if now != src_bytes:
            probs.append("the input file changed during the run")
        if fw2.get("head") != fw.get("head") or fw2["ok"] != fw["ok"]:
            probs.append("the framework checkout changed during the run")
        if probs:
            rep.set("integrity", "FAIL", "; ".join(probs))
        else:
            rep.set("integrity", "PASS", "input sha256 and framework HEAD/cleanliness identical before and after")
    else:
        rep.set("integrity", "FAIL", "not run: input unreadable")

    # ---- verdict
    failed = rep.failed()
    if failed:
        result, exitc = "FAIL", 1
    elif o["text_only"]:
        bad = [c for c in text_ids + ("framework", "integrity") if rep.status(c) != "PASS"]
        result, exitc = ("FAIL", 1) if bad else ("TEXT_ONLY_OK", 4)
    elif o["selftest"]:
        result, exitc = "SELFTEST_OK", 5
    elif o["emit"]:
        others = [c for c in rep.order if c != "assumptions" and rep.status(c) != "PASS"
                  and not (c == "coqchk" and ctx.get("coqchk_outcome") == "timeout")]   # policy A
        result, exitc = ("FAIL", 1) if others else ("BASELINE_SKIPPED", 3)
    elif all(rep.status(c) == "PASS" or (c == "coqchk" and ctx.get("coqchk_outcome") == "timeout")
             for c in rep.order):   # policy A: a coqchk timeout is the one allowed non-PASS
        result, exitc = "PASS", 0
    else:
        result, exitc = "FAIL", 1
    assert (exitc == 0) == (result == "PASS"), (result, exitc)   # 0 is the kill signal, and only that

    summary = {
        "tool": "check_kill", "tool_version": TOOL_VERSION, "result": result, "exit": exitc,
        "file": path, "sha256": rep.meta.get("sha256"), "tm": tm, "mode": mode, "theorem": thm,
        "framework_head": rep.meta.get("framework_head"), "coqc": ctx.get("coqc"),
        "coqc_version": ctx.get("coqc_version"), "compile_seconds": ctx.get("compile_seconds"),
        "native_compiler": ctx.get("native"),
        "coqchk": ctx["coqchk_outcome"] if o["coqchk"] and not o["text_only"] else False,
        "coqchk_timeout": o["coqchk_timeout"] if o["coqchk"] and not o["text_only"] else None,
        "coqchk_seconds": ctx.get("coqchk_seconds"),
        "ml_modules": ctx.get("ml_modules"),
        "fqns": ctx.get("fqns"), "assumptions": ctx.get("assumptions"),
        "checked_at": datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ"),
        "checks": [{k: rep.checks[c][k] for k in ("id", "status", "summary", "details", "warnings")}
                   for c in rep.order],
    }
    if summary["coqchk"] is not False:   # the enum documented at TOOL_VERSION matches check (h)'s status
        assert COQCHK_OUTCOMES[summary["coqchk"]] == rep.status("coqchk"), (summary["coqchk"], rep.status("coqchk"))
    if o["keep"] and ctx.get("tmp"):
        summary["temp_dir"] = ctx["tmp"]
    text = render(rep, o, result, exitc, ctx)
    js = json.dumps(summary, ensure_ascii=True, separators=(",", ":"))
    if o["json"]:
        print(text, file=sys.stderr)
        print(js)
    else:
        print(text)
        print("JSON: " + js)
    return exitc


if __name__ == "__main__":
    try:
        sys.exit(main())
    except KeyboardInterrupt:
        print("check_kill: interrupted", file=sys.stderr)
        sys.exit(2)
CHECK_KILL_PY