#!/usr/bin/env python3
"""Read-only static preflight. This deliberately does not certify Lean proofs."""
import argparse
import json
import re
from datetime import datetime, timezone
from pathlib import Path


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("--source", required=True, type=Path)
    parser.add_argument("--inventory", required=True, type=Path)
    parser.add_argument("--output", required=True, type=Path)
    args = parser.parse_args()
    inventory = json.loads(args.inventory.read_text())
    lean = args.source / "lean"
    configurations = []
    for path in sorted((lean / "ComparatorChallenges").glob("*.json")):
        config = json.loads(path.read_text())
        modules = {}
        for key in ["challenge_module", "solution_module"]:
            name = config.get(key)
            resolved = lean.joinpath(*name.split(".")).with_suffix(".lean") if name else None
            modules[key] = {"module": name, "exists": bool(resolved and resolved.exists()),
                            "path": str(resolved.relative_to(args.source)) if resolved and resolved.exists() else None}
        configurations.append({"config": str(path.relative_to(args.source)), "modules": modules,
                               "theorem_names": config.get("theorem_names", []),
                               "definition_names": config.get("definition_names", []),
                               "permitted_axioms": config.get("permitted_axioms", []),
                               "external_kernel_enabled": bool(config.get("enable_nanoda") or config.get("external_kernels")),
                               "verification": "NOT_RUN"})
    families = []
    for family in inventory["families"]:
        scope_path = family["lean_scope_path"]
        scope = (args.source / scope_path).read_text() if scope_path else ""
        links = re.findall(r"\]\(\.\./ComparatorChallenges/([^)]*\.lean)\)", scope)
        flags = []
        for needle, flag in [("outside", "scope_exclusion"), ("not included", "scope_exclusion"),
                             ("supporting", "supporting_result"), ("unrestricted computation", "query_model_only"),
                             ("arithmetic and bit costs are not bounded", "query_model_only"),
                             ("practical", "practical_cost_limitation"), ("150020", "huge_polynomial_degree")]:
            if needle.lower() in scope.lower() and flag not in flags:
                flags.append(flag)
        manuscript_sources = []
        for paper in family["papers"]:
            folder = (args.source / paper["path"]).parent
            files = [f for f in folder.rglob("*.tex") if "runtime" not in f.parts and not any(part in {".lake", "texmf"} for part in f.parts)]
            manuscript_sources.append({"paper": paper["path"], "tex_paths": [str(f.relative_to(args.source)) for f in sorted(files)]})
        families.append({"family_id": family["family_id"], "scope_path": scope_path, "comparator_challenges": sorted(set(links)),
                         "flags": flags, "manuscript_source_files": manuscript_sources, "verification": "NOT_RUN"})
    missing = [c["config"] for c in configurations if any(not m["exists"] for m in c["modules"].values())]
    report = {"mode": "STATIC_METADATA_ONLY", "source_commit": inventory["metadata"]["source_commit"],
              "created_at_utc": datetime.now(timezone.utc).isoformat(),
              "summary": {"configs": len(configurations), "families": len(families), "missing_module_configs": missing,
                          "external_kernel_enabled_configs": sum(c["external_kernel_enabled"] for c in configurations)},
              "limits": ["No Lean compilation or Comparator execution was performed.",
                         "Scope flags are keyword diagnostics requiring manual interpretation.",
                         "Challenge placeholders are expected and do not imply invalid solution proofs.",
                         "Module existence does not establish theorem equivalence, allowed axiom use, or correctness."],
              "configs": configurations, "families": families}
    args.output.parent.mkdir(parents=True, exist_ok=True)
    with args.output.open("x") as stream:
        json.dump(report, stream, ensure_ascii=False, indent=2)
        stream.write("\n")
    print(json.dumps(report["summary"], indent=2))


if __name__ == "__main__":
    main()