#!/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)
- complétion_minorée_m14_vers_m15.md (contains both-parent list at 2^14 + residual list at 2^15)
- complétion_minorée_m15_vers_m16.md (contains both-parent list at 2^15)

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 verify_c2(
    *,
    noyau_both_base_4096_md: Path,
    completion_m14_to_m15_md: Path,
    completion_m15_to_m16_md: Path,
    repo_root: Path,
    output_json: Path,
    output_md: Path,
) -> None:
    b12_md = _read_text(noyau_both_base_4096_md)
    c1415_md = _read_text(completion_m14_to_m15_md)
    c1516_md = _read_text(completion_m15_to_m16_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)}")

    # m=14 -> m=15
    both14 = _parse_list_under_heading(c1415_md, r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^14\b")
    _assert_all_odd(both14, "Parents both (m=14)")
    children15 = _lift_children(both14, 14)
    _assert_all_odd(children15, "Computed children at m=15")

    residual15 = _parse_list_under_heading(
        c1415_md,
        r"^###\s+Résidu\s+restant\s+au\s+palier\s+2\^15\s+après\s+complétion\s+«\s+one\s+»",
    )
    _assert_all_odd(residual15, "Listed residual at m=15")

    c1415 = C2CheckResult(
        palier_parent=14,
        palier_child=15,
        both_parent_count=len(both14),
        computed_children_count=len(children15),
        listed_residual_count=len(residual15),
        children_equals_listed_residual=(set(children15) == set(residual15)),
        projection_mod_4096_equals_b12=(_project_mod_4096(both14) == set(b12)),
    )

    # m=15 -> m=16
    both15 = _parse_list_under_heading(c1516_md, r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^15\b")
    _assert_all_odd(both15, "Parents both (m=15)")
    children16 = _lift_children(both15, 15)
    _assert_all_odd(children16, "Computed children at m=16")

    # This completion file does not necessarily list the full residual after completion, so we only check the count.
    c1516 = C2CheckResult(
        palier_parent=15,
        palier_child=16,
        both_parent_count=len(both15),
        computed_children_count=len(children16),
        listed_residual_count=None,
        children_equals_listed_residual=None,
        projection_mod_4096_equals_b12=(_project_mod_4096(both15) == set(b12)),
    )

    summary = {
        "inputs": {
            "noyau_both_base_4096_md": _display_path(noyau_both_base_4096_md, repo_root),
            "completion_m14_to_m15_md": _display_path(completion_m14_to_m15_md, repo_root),
            "completion_m15_to_m16_md": _display_path(completion_m15_to_m16_md, repo_root),
        },
        "B12": {"count": len(b12), "min": min(b12), "max": max(b12)},
        "checks": {
            "m14_to_m15": c1415.__dict__,
            "m15_to_m16": c1516.__dict__,
        },
        "ok": {
            "m14_to_m15_children_equals_listed_residual": bool(c1415.children_equals_listed_residual),
            "m14_projection_equals_b12": bool(c1415.projection_mod_4096_equals_b12),
            "m15_projection_equals_b12": bool(c1516.projection_mod_4096_equals_b12),
        },
    }

    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)}`")
    lines.append(f"- `complétion_minorée_m14_vers_m15.md` : `{_display_path(completion_m14_to_m15_md, repo_root)}`")
    lines.append(f"- `complétion_minorée_m15_vers_m16.md` : `{_display_path(completion_m15_to_m16_md, 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("## Transition m=14 → m=15 (complétion par frères ⇒ résidu = enfants des both)")
    lines.append("")
    lines.append(f"- |both parents (m=14)| = {c1415.both_parent_count}")
    lines.append(f"- |computed children (m=15)| = {c1415.computed_children_count} (attendu 2*|both|)")
    lines.append(f"- |listed residual (m=15)| = {c1415.listed_residual_count}")
    lines.append(f"- computed children == listed residual : {c1415.children_equals_listed_residual}")
    lines.append(f"- projection both(m=14) mod 4096 == B12 : {c1415.projection_mod_4096_equals_b12}")
    lines.append("")
    lines.append("## Transition m=15 → m=16 (projection des both)")
    lines.append("")
    lines.append(f"- |both parents (m=15)| = {c1516.both_parent_count}")
    lines.append(f"- |computed children (m=16)| = {c1516.computed_children_count} (attendu 2*|both|)")
    lines.append(f"- projection both(m=15) mod 4096 == B12 : {c1516.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(
        "--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(
        "--completion-m14-to-m15-md",
        default=str(Path(__file__).parent / "complétion_minorée_m14_vers_m15.md"),
        help="Path to complétion_minorée_m14_vers_m15.md",
    )
    ap.add_argument(
        "--completion-m15-to-m16-md",
        default=str(Path(__file__).parent / "complétion_minorée_m15_vers_m16.md"),
        help="Path to complétion_minorée_m15_vers_m16.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()
    out_dir = Path(args.output_dir)
    verify_c2(
        noyau_both_base_4096_md=Path(args.noyau_both_base_4096_md),
        completion_m14_to_m15_md=Path(args.completion_m14_to_m15_md),
        completion_m15_to_m16_md=Path(args.completion_m15_to_m16_md),
        repo_root=repo_root,
        output_json=out_dir / "verification_c2_projective.json",
        output_md=out_dir / "verification_c2_projective.md",
    )


if __name__ == "__main__":
    main()