XZBT/tools/verify-spec-contract.py

#!/usr/bin/env python3
"""Contract verification harness for XZBT_0-1_Format_Specification.md.

Checks, over the whole document:
  1. every ERR_*/WARN_*/INFO_* code used resolves to a row of the section 7 table;
  2. every section 7 row is used at least once outside the table;
  3. every numeric cross-reference (e.g. "section 19.5", "19.5", "17.16.14") resolves
     to a real heading or a numbered trace item;
  4. code fences balance;
  5. markdown table rows are well formed (consistent column count per table,
     discounting escaped pipes).

Exit status is non-zero when any check fails.
"""
import io, os, re, sys, collections

SPEC = os.path.join(os.path.dirname(os.path.abspath(__file__)),
                    "..", "docs", "XZBT_0-1_Format_Specification.md")

def main():
    text = io.open(SPEC, encoding="utf-8").read()
    lines = text.split("\n")
    problems = []

    # ---- fences -------------------------------------------------------
    fence_lines = [i for i, l in enumerate(lines, 1) if l.strip().startswith("```")]
    if len(fence_lines) % 2:
        problems.append("unbalanced code fences: %d fence markers" % len(fence_lines))
    in_fence = set()
    for a, b in zip(fence_lines[0::2], fence_lines[1::2]):
        in_fence.update(range(a, b + 1))

    # ---- headings -----------------------------------------------------
    headings = {}
    for i, l in enumerate(lines, 1):
        m = re.match(r"^#{2,4}\s+(\d+(?:\.\d+)*)\.?\s", l)
        if m:
            headings[m.group(1)] = i
    # numbered trace items inside a "Required traces" subsection
    trace_items = collections.defaultdict(set)
    current = None
    for i, l in enumerate(lines, 1):
        m = re.match(r"^#{2,4}\s+(\d+(?:\.\d+)*)\.?\s", l)
        if m:
            current = m.group(1)
            continue
        if current and re.match(r"^(\d+)\.\s", l) and i not in in_fence:
            trace_items[current].add(re.match(r"^(\d+)\.\s", l).group(1))

    # ---- section 7 diagnostic table ------------------------------------
    declared = set()
    sec7 = headings.get("7")
    if not sec7:
        problems.append("section 7 heading not found")
    else:
        i = sec7
        while i < len(lines) and not re.match(r"^## 8\.", lines[i]):
            m = re.match(r"^\|\s*`((?:ERR|WARN|INFO)_[A-Z0-9_]+)`\s*\|", lines[i])
            if m:
                declared.add(m.group(1))
            i += 1

    used = collections.Counter()
    for i, l in enumerate(lines, 1):
        if sec7 and sec7 <= i < sec7 + 60 and re.match(r"^\|\s*`(?:ERR|WARN|INFO)_", l):
            continue
        for code in re.findall(r"`((?:ERR|WARN|INFO)_[A-Z0-9_]+)`", l):
            used[code] += 1

    for code in sorted(used):
        if code not in declared:
            problems.append("undeclared diagnostic code used: %s" % code)
    declared_only = sorted(c for c in declared if c not in used)

    # ---- cross references ---------------------------------------------
    xrefs = collections.Counter()
    for i, l in enumerate(lines, 1):
        if i in in_fence:
            continue
        if re.match(r"^\|?\s*`?(?:ERR|WARN|INFO)_", l):
            pass
        scan = re.sub(r"`[^`]*`", " ", l)   # inline code spans hold data, not references
        for m in re.finditer(r"(?<![\w.\-/])(\d{1,2}\.\d{1,2}(?:\.\d{1,2})?)(?![\w.\-])", scan):
            ref = m.group(1)
            head = ref.split(".")[0]
            if head not in ("1","2","3","4","5","6","7","8","9","10","11","12","13",
                            "14","15","16","17","18","19"):
                continue
            xrefs[ref] += 1

    unresolved = []
    for ref in sorted(xrefs):
        if ref in headings:
            continue
        parts = ref.split(".")
        if len(parts) == 3:
            parent = parts[0] + "." + parts[1]
            if parent in headings and parts[2] in trace_items.get(parent, set()):
                continue
        unresolved.append(ref)

    # ---- tables --------------------------------------------------------
    tbl_start = None
    tbl_cols = None
    tables = 0
    for i, l in enumerate(lines, 1):
        if i in in_fence:
            continue
        is_row = l.lstrip().startswith("|") and l.rstrip().endswith("|")
        if is_row:
            cols = len(re.findall(r"(?<!\\)\|", l)) - 1
            if tbl_start is None:
                tbl_start, tbl_cols = i, cols
                tables += 1
            elif cols != tbl_cols:
                problems.append("line %d: table starting at line %d has %d columns here, %d at its head"
                                % (i, tbl_start, cols, tbl_cols))
        else:
            tbl_start, tbl_cols = None, None

    print("headings:            %d" % len(headings))
    print("diagnostic codes:    %d declared, %d distinct used" % (len(declared), len(used)))
    print("cross-references:    %d distinct, %d unresolved" % (len(xrefs), len(unresolved)))
    print("code fences:         %d markers (%s)" % (len(fence_lines),
          "balanced" if len(fence_lines) % 2 == 0 else "UNBALANCED"))
    print("tables:              %d" % tables)
    if declared_only:
        print("declared-only codes: %s" % ", ".join(declared_only))
    if unresolved:
        print("\nunresolved cross-references:")
        for r in unresolved:
            print("  %s (%d use%s)" % (r, xrefs[r], "" if xrefs[r] == 1 else "s"))
    if problems:
        print("\nproblems:")
        for p in problems:
            print("  " + p)
    if problems or unresolved:
        return 1
    print("\nOK — every code resolves, every cross-reference resolves, fences balanced, tables well formed.")
    return 0

if __name__ == "__main__":
    sys.exit(main())