"""Gate the bounded frontier delta on executed evidence, validate, then zip.

This packages an already reviewed theorem application; it is not a formal
proof checker for the external theorems or for their mathematical use.
"""
import argparse
import ast
import hashlib
import json
import re
import zipfile
from datetime import datetime, timezone
from pathlib import Path

ROOT = Path(__file__).resolve().parents[1]


def sha(path):
    return hashlib.sha256(path.read_bytes()).hexdigest()


def read(relative):
    return json.loads((ROOT/relative).read_text(encoding="utf-8"))


def require(condition, message):
    if not condition:
        raise ValueError(message)


def write(relative, value):
    path = ROOT/relative
    path.parent.mkdir(parents=True, exist_ok=True)
    path.write_text(json.dumps(value, ensure_ascii=False, indent=2, sort_keys=True)+"\n", encoding="utf-8")


def entries():
    return sorted(p for p in ROOT.rglob("*") if p.is_file()
                  and "__pycache__" not in p.parts and p.suffix != ".pyc"
                  and "replay_checks" not in p.relative_to(ROOT).parts)


def finalize(zip_path):
    independent = read("results/independent_verification.json")
    fresh = read("results/fresh_replay.json")
    negative = read("results/independent_negative_checks.json")
    prior = read("results/prior_input_replay.json")
    require(all(r.get("verdict") == "PASS" for r in [independent,fresh,negative,prior]),
            "FRONTIER_GATE: a required report is not PASS")
    require(fresh["independent_verification"]["verdict"] == "PASS" and
            fresh["prior_input_replay"] == prior, "FRONTIER_GATE: fresh premises differ")
    require([s["step"] for s in fresh["steps"]] ==
            ["C1_FRESH_PRODUCER", "C2_INDEPENDENT_FULL_REPLAY", "C4_PRIOR_INPUTS", "C5_EXACT_AND_MUTATION_TESTS"],
            "FRONTIER_GATE: incomplete execution sequence")
    require(all(s["returncode"] == 0 for s in fresh["steps"]), "FRONTIER_GATE: failed command")
    require("Ran 11 tests" in fresh["steps"][-1]["stderr"], "FRONTIER_GATE: incomplete test count")
    for name, item in fresh["core_file_comparisons"].items():
        require(item["identical"] and item["fresh_sha256"] == item["shipped_sha256"] == sha(ROOT/"results"/name),
                f"FRONTIER_GATE: changed core file {name}")
    require(len(fresh["core_file_comparisons"]) == 4, "FRONTIER_GATE: missing core comparisons")
    for relative, wanted in fresh["source_sha256"].items():
        require(sha(ROOT/relative) == wanted, f"FRONTIER_GATE: tested source changed: {relative}")
    require(negative["rejected_mutation_count"] == len(negative["mutations"]) == 9 and
            all(x["verdict"] == "REJECTED" and x["all_binding_hashes_resealed"] and "hash" not in x["failed_step"]
                for x in negative["mutations"]), "FRONTIER_GATE: inadequate mutation evidence")
    require(independent["summation"]["unit_count"] == 392040 and
            independent["summation"]["residue"] == 5 and
            independent["summation"]["all_csv_rows_independently_recomputed"],
            "FRONTIER_GATE: missing full finite replay")
    now = datetime.now(timezone.utc)
    require(now > datetime.fromisoformat(fresh["finished_utc"]), "FRONTIER_GATE: update precedes replay")
    evidence_paths = ["results/independent_verification.json", "results/fresh_replay.json",
                      "results/independent_negative_checks.json", "results/prior_input_replay.json",
                      "notes/twin_final_review.md", "02_CANONICAL_FRONTIER_DELTA.md"]
    delta = {
        "schema": "kurihara-canonical-frontier-delta-v1",
        "updated_utc": now.isoformat(), "gate_verdict": "PASS",
        "gate_basis": "Executed fresh reconstruction, independent full replay, exact byte equality, all 11 tests, 9 resealed rejected mutations",
        "previous_result": read("provenance/input_hashes.json")["previous_result_zip"],
        "evidence_sha256": {relative: sha(ROOT/relative) for relative in evidence_paths},
        "updates": [
            {"claim_id": "R304", "status": "VERIFIED_FINITE",
             "statement": "Manin rank325, quotient65, joint Hecke dimension2, geometric plus dimension1"},
            {"claim_id": "R305", "status": "NOT_REPRODUCED_NORMALIZATION_UNSPECIFIED",
             "statement": "The archival literal residue6 has no identifiable normalization in the supplied archive"},
            {"claim_id": "K501", "status": "VERIFIED_FINITE", "replaces_dependency": "R305 nonvanishing component only",
             "statement": "Fixed first-nonzero normalization lambda(1,5)=1 and roots5,6 give delta393427=5 mod11"},
            {"claim_id": "K502", "status": "VERIFIED_THEOREM_APPLICATION", "depends_on": ["R304","K501","R307"],
             "statement": "The canonical conductor393427 value is5u mod11 with u in F11*, hence nonzero; absolute u not computed"},
            {"claim_id": "R308", "status": "VERIFIED_THEOREM_APPLICATION", "depends_on": ["K502","R307","R313"],
             "statement": "Mordell-Weil rank=Selmer corank=2 and Sha[11^infinity]=0, using Kim1.8(1),(3) without assuming Sha finiteness"},
            {"claim_id": "R314", "status": "VERIFIED_THEOREM_APPLICATION", "depends_on": ["R308","R313"],
             "statement": "Full Sel11=span(P,Q); specified norm-cube dimensions2,1,1,0"}
        ],
        "unchanged": {"R307": "VERIFIED_THEOREM_APPLICATION_FROM_PREVIOUS_ROUND",
                      "R315": "UNVERIFIED", "R317": "CONDITIONAL",
                      "R318_CANON_BocID": "OPEN", "R319_CPLX_GPR": "OPEN"},
        "theorem_check_boundary": "External theorem applications are reviewed in the mathematical note, not proved by Python."
    }
    write("results/frontier_delta.json", delta)

    checked = {"utf8_text_files": 0, "json_files": 0, "python_files": 0, "markdown_files": 0}
    excluded = {"SHA256SUMS", "results/package_validation.json"}
    for path in entries():
        relative = str(path.relative_to(ROOT))
        if relative in excluded:
            continue
        if path.suffix in (".py", ".md", ".json", ".txt", ".csv"):
            text = path.read_text(encoding="utf-8")
            checked["utf8_text_files"] += 1
            require("\ufffd" not in text, f"UTF8: replacement character in {relative}")
            if path.suffix == ".py":
                ast.parse(text, filename=relative)
                checked["python_files"] += 1
            elif path.suffix == ".json":
                json.loads(text)
                checked["json_files"] += 1
            elif path.suffix == ".md":
                # A doubled backslash before '(' is a math row break, not a delimiter.
                require(not re.search(r"(?<!\\)\\[()\[\]]", text), f"MATH_DELIMITERS: {relative}")
                require(len(re.findall(r"(?<!\\)\$\$", text)) % 2 == 0,
                        f"MATH_BLOCKS: unpaired display delimiter in {relative}")
                checked["markdown_files"] += 1
    validation = {"schema": "kurihara-package-validation-v1", "verdict": "PASS",
                  "checks": checked, "tested_source_hashes_match": True,
                  "core_certificate_hashes_match_fresh_replay": True,
                  "frontier_updated_after_successful_replay": True,
                  "all_math_reports_pass": True,
                  "scope": "Package integrity, executable evidence gate, UTF-8 and canonical math delimiters"}
    write("results/package_validation.json", validation)
    manifest = [(str(p.relative_to(ROOT)), sha(p)) for p in entries() if p.name != "SHA256SUMS"]
    (ROOT/"SHA256SUMS").write_text("".join(f"{digest}  {relative}\n" for relative, digest in manifest), encoding="utf-8")
    zip_path = zip_path.resolve()
    require(ROOT not in zip_path.parents, "ZIP_PATH: output must be outside the package directory")
    zip_path.parent.mkdir(parents=True, exist_ok=True)
    with zipfile.ZipFile(zip_path, "w", compression=zipfile.ZIP_DEFLATED, compresslevel=9) as bundle:
        for path in entries():
            bundle.write(path, Path(ROOT.name)/path.relative_to(ROOT))
    with zipfile.ZipFile(zip_path) as bundle:
        require(bundle.testzip() is None, "ZIP_CRC: corrupted member")
        for relative, wanted in manifest:
            observed = hashlib.sha256(bundle.read(str(Path(ROOT.name)/relative))).hexdigest()
            require(observed == wanted, f"ZIP_HASH: {relative}")
        count = len(bundle.namelist())
    return {"verdict": "PASS", "zip": str(zip_path), "zip_sha256": sha(zip_path),
            "zip_bytes": zip_path.stat().st_size, "file_count": count, "validation": validation}


if __name__ == "__main__":
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--zip", type=Path, required=True)
    args = parser.parse_args()
    print(json.dumps(finalize(args.zip), ensure_ascii=False, indent=2, sort_keys=True))