#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
collatz_verify_c2_projective.py

Deterministic verification artefact for Lemma C2 (projective reduction):

From completion-by-brothers audit documents, verify that:
- residual after completion equals the set of children of "both" parents
- projections modulo 2^12 of B_m (both parents) match the fixed base B12

Inputs (Markdown):
- noyau_both_base_4096.md (contains B12 list)
- completion documents (e.g. complétion_minorée_m14_vers_m15.md, complétion_minorée_m15_vers_m16.md)

Outputs:
- a short JSON summary (machine-checkable)
- a short Markdown report (human-checkable)

No terminal transcripts. Standard library only.
"""

from __future__ import annotations

import argparse
import json
import re
from dataclasses import dataclass
from pathlib import Path


def _read_text(path: Path) -> str:
    return path.read_text(encoding="utf-8", errors="strict")


def _extract_ints(text: str) -> list[int]:
    return [int(x) for x in re.findall(r"\b\d+\b", text)]


def _section_after_heading(md: str, heading_regex: str) -> str:
    """
    Return the Markdown slice starting at a heading matched by heading_regex (regex applied line-wise).
    The slice ends at the next heading of same or higher level, or end of document.
    """
    lines = md.splitlines()
    start = None
    level = None
    hr = re.compile(heading_regex)
    for i, line in enumerate(lines):
        if hr.search(line):
            start = i + 1
            m = re.match(r"^(#+)\s", line)
            level = len(m.group(1)) if m else 1
            break
    if start is None or level is None:
        raise ValueError(f"Cannot find heading matching regex: {heading_regex}")

    end = len(lines)
    for j in range(start, len(lines)):
        m2 = re.match(r"^(#+)\s", lines[j])
        if not m2:
            continue
        if len(m2.group(1)) <= level:
            end = j
            break
    return "\n".join(lines[start:end]).strip()


def _parse_list_under_heading(md: str, heading_regex: str) -> list[int]:
    section = _section_after_heading(md, heading_regex)
    return sorted(set(_extract_ints(section)))


def _assert_all_odd(values: list[int], label: str) -> None:
    bad = [x for x in values if x % 2 == 0]
    if bad:
        raise ValueError(f"{label}: expected odd residues only, found {len(bad)} even values (e.g. {bad[:10]})")


@dataclass(frozen=True)
class C2CheckResult:
    palier_parent: int
    palier_child: int
    both_parent_count: int
    computed_children_count: int
    listed_residual_count: int | None
    children_equals_listed_residual: bool | None
    projection_mod_4096_equals_b12: bool


def _lift_children(both_parents: list[int], parent_palier: int) -> list[int]:
    shift = 1 << parent_palier
    out = set()
    for p in both_parents:
        out.add(p)
        out.add(p + shift)
    return sorted(out)


def _project_mod_4096(values: list[int]) -> set[int]:
    return {int(x % 4096) for x in values}


def _display_path(path: Path, repo_root: Path) -> str:
    try:
        rel = path.resolve().relative_to(repo_root.resolve())
        return str(rel)
    except ValueError:
        return str(path)


def _discover_both_parent_blocks(md: str) -> dict[int, list[int]]:
    """
    Discover "Parents « both » au palier 2^m" blocks in a completion markdown file.
    Returns m -> residues list.
    """
    out: dict[int, list[int]] = {}
    for m in re.findall(r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^(\d+)\b", md, flags=re.M):
        mm = int(m)
        out[mm] = _parse_list_under_heading(
            md, rf"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^{mm}\b"
        )
    return out


def _discover_listed_residual_after_completion(md: str, child_palier: int) -> list[int] | None:
    """
    Optional: "Résidu restant au palier 2^(m+1) après complétion « one » (...)".
    """
    pattern = rf"^###\s+Résidu\s+restant\s+au\s+palier\s+2\^{child_palier}\s+après\s+complétion\s+«\s+one\s+»"
    try:
        return _parse_list_under_heading(md, pattern)
    except ValueError:
        return None


def _discover_declared_residual_size(md: str, child_palier: int) -> int | None:
    """
    Optional: parse a declared residual size like "|R_16^comp| = 2202".
    """
    matches = re.findall(rf"\|R_{child_palier}\^comp\|\s*=\s*([^\n]+)", md)
    if not matches:
        return None
    # Extract the last integer on the matched RHS (e.g. "2*|both| = 2202" -> 2202).
    rhs = matches[-1]
    ints = re.findall(r"\b(\d+)\b", rhs)
    return int(ints[-1]) if ints else None


def verify_c2(
    *,
    noyau_both_base_4096_md: Path,
    completion_docs: list[Path],
    repo_root: Path,
    output_json: Path,
    output_md: Path,
) -> None:
    b12_md = _read_text(noyau_both_base_4096_md)

    b12 = _parse_list_under_heading(b12_md, r"^##\s+Base projective B_12\b")
    _assert_all_odd(b12, "B12")
    if len(b12) != 192:
        raise ValueError(f"B12: expected 192 residues, got {len(b12)}")

    transitions: list[dict[str, object]] = []
    for doc_path in completion_docs:
        md = _read_text(doc_path)
        src = _display_path(doc_path, repo_root)
        both_blocks = _discover_both_parent_blocks(md)
        for m_parent, both in sorted(both_blocks.items()):
            _assert_all_odd(both, f"Parents both (m={m_parent}) in {src}")
            child_palier = m_parent + 1
            children = _lift_children(both, m_parent)
            _assert_all_odd(children, f"Computed children (m={child_palier}) in {src}")

            listed = _discover_listed_residual_after_completion(md, child_palier)
            declared = _discover_declared_residual_size(md, child_palier)
            if listed is not None:
                _assert_all_odd(listed, f"Listed residual (m={child_palier}) in {src}")
                if set(children) != set(listed):
                    raise ValueError(
                        f"Residual list mismatch for m={m_parent}→{child_palier} in {src}: "
                        "listed residual does not match computed children of both"
                    )
            if declared is not None and declared != len(children):
                raise ValueError(
                    f"Declared |R_{child_palier}^comp|={declared} does not match computed {len(children)} for {src}"
                )

            transitions.append(
                {
                    "source": src,
                    "palier_parent": m_parent,
                    "palier_child": child_palier,
                    "both_parent_count": len(both),
                    "computed_children_count": len(children),
                    "listed_residual_count": len(listed) if listed is not None else declared,
                    "children_equals_listed_residual": (set(children) == set(listed)) if listed is not None else None,
                    "projection_mod_4096_equals_b12": (_project_mod_4096(both) == set(b12)),
                }
            )

    # Stable ordering for deterministic JSON/MD
    transitions = sorted(
        transitions,
        key=lambda d: (str(d["source"]), int(d["palier_parent"]), int(d["palier_child"])),
    )

    def _pick_check(parent_m: int) -> C2CheckResult:
        matches = [t for t in transitions if int(t["palier_parent"]) == parent_m and int(t["palier_child"]) == parent_m + 1]
        if not matches:
            raise ValueError(f"Missing expected transition m={parent_m}→{parent_m+1} in discovered completion docs")
        # deterministic: pick first by our transition ordering
        t = matches[0]
        return C2CheckResult(
            palier_parent=int(t["palier_parent"]),
            palier_child=int(t["palier_child"]),
            both_parent_count=int(t["both_parent_count"]),
            computed_children_count=int(t["computed_children_count"]),
            listed_residual_count=(int(t["listed_residual_count"]) if t["listed_residual_count"] is not None else None),
            children_equals_listed_residual=(bool(t["children_equals_listed_residual"]) if t["children_equals_listed_residual"] is not None else None),
            projection_mod_4096_equals_b12=bool(t["projection_mod_4096_equals_b12"]),
        )

    # Backward-compatible checks block for report generator / downstream tooling.
    c1415 = _pick_check(14)
    c1516 = _pick_check(15)

    summary = {
        "inputs": {
            "noyau_both_base_4096_md": _display_path(noyau_both_base_4096_md, repo_root),
            "completion_docs": [_display_path(p, repo_root) for p in completion_docs],
        },
        "B12": {"count": len(b12), "min": min(b12), "max": max(b12)},
        "transitions": transitions,
        "checks": {
            "m14_to_m15": c1415.__dict__,
            "m15_to_m16": c1516.__dict__,
        },
        "ok": {
            "all_transitions_project_to_B12": all(bool(t["projection_mod_4096_equals_b12"]) for t in transitions),
            "all_listed_residuals_match_children": all(
                (t["children_equals_listed_residual"] is None) or bool(t["children_equals_listed_residual"])
                for t in transitions
            ),
        },
    }

    output_json.parent.mkdir(parents=True, exist_ok=True)
    output_json.write_text(json.dumps(summary, indent=2, ensure_ascii=False) + "\n", encoding="utf-8")

    lines: list[str] = []
    lines.append("**Auteur** : Équipe 4NK")
    lines.append("")
    lines.append("# Vérification déterministe — Lemma C2 (réduction projective)")
    lines.append("")
    lines.append("## Entrées")
    lines.append("")
    lines.append(f"- `noyau_both_base_4096.md` : `{_display_path(noyau_both_base_4096_md, repo_root)}`")
    for p in completion_docs:
        lines.append(f"- completion : `{_display_path(p, repo_root)}`")
    lines.append("")
    lines.append("## Base projective B12")
    lines.append("")
    lines.append(f"- |B12| = {len(b12)} (attendu 192)")
    lines.append(f"- min(B12) = {min(b12)}, max(B12) = {max(b12)}")
    lines.append("")
    lines.append("## Transitions détectées (table multi-transitions)")
    lines.append("")
    header = [
        "source",
        "m",
        "m+1",
        "|both(m)|",
        "|children(m+1)|",
        "|listed residual|",
        "children==listed",
        "both mod 4096 == B12",
    ]
    lines.append("| " + " | ".join(header) + " |")
    lines.append("| " + " | ".join(["---"] * len(header)) + " |")
    for t in transitions:
        lines.append(
            "| "
            + " | ".join(
                [
                    str(t["source"]),
                    str(t["palier_parent"]),
                    str(t["palier_child"]),
                    str(t["both_parent_count"]),
                    str(t["computed_children_count"]),
                    str(t["listed_residual_count"]) if t["listed_residual_count"] is not None else "",
                    str(t["children_equals_listed_residual"]) if t["children_equals_listed_residual"] is not None else "",
                    str(t["projection_mod_4096_equals_b12"]),
                ]
            )
            + " |"
        )
    lines.append("")
    lines.append("## Sorties")
    lines.append("")
    lines.append(f"- JSON : `{output_json}`")
    lines.append(f"- Markdown : `{output_md}`")
    lines.append("")

    output_md.parent.mkdir(parents=True, exist_ok=True)
    output_md.write_text("\n".join(lines) + "\n", encoding="utf-8")


def main() -> None:
    ap = argparse.ArgumentParser(description="Deterministic C2 verification (projective reduction)")
    ap.add_argument(
        "--repo-root",
        default="",
        help="Repository root used to display relative paths in outputs (defaults to current working directory)",
    )
    ap.add_argument(
        "--completion-dir",
        default="",
        help="Directory to auto-discover completion markdown files (default: collatz_k_scripts directory)",
    )
    ap.add_argument(
        "--completion-md",
        action="append",
        default=[],
        help="Completion markdown file (repeatable). If provided, disables auto-discovery.",
    )
    ap.add_argument(
        "--noyau-both-base-4096-md",
        default=str(Path(__file__).parent / "noyau_both_base_4096.md"),
        help="Path to noyau_both_base_4096.md",
    )
    ap.add_argument(
        "--output-dir",
        default="docs/artefacts/collatz/c2_projective",
        help="Output directory for deterministic artefacts (JSON + MD)",
    )
    args = ap.parse_args()

    repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve()
    completion_docs: list[Path]
    if args.completion_md:
        completion_docs = [Path(p).resolve() for p in args.completion_md]
    else:
        completion_dir = Path(args.completion_dir).resolve() if args.completion_dir.strip() else Path(__file__).parent.resolve()
        completion_docs = sorted(completion_dir.glob("complétion*_m*_vers_m*.md"))
        if not completion_docs:
            raise ValueError(f"No completion docs found under {completion_dir}")

    out_dir = Path(args.output_dir)
    verify_c2(
        noyau_both_base_4096_md=Path(args.noyau_both_base_4096_md),
        completion_docs=completion_docs,
        repo_root=repo_root,
        output_json=out_dir / "verification_c2_projective.json",
        output_md=out_dir / "verification_c2_projective.md",
    )


if __name__ == "__main__":
    main()