#!/usr/bin/env python3
"""Hostile source and certificate audit for C-0050."""

from __future__ import annotations

import ast
import hashlib
import importlib.util
from importlib.metadata import version
import json
import math
from math import factorial
from pathlib import Path
import platform
import re
import subprocess
import sys
from fractions import Fraction

import flint
from flint import arb


if not __debug__:
    raise RuntimeError("optimized Python is unsupported for verification")


HERE = Path(__file__).resolve().parent
SOURCE = HERE / "source"
ORIGINAL = SOURCE / "repository" / "original-verify.py"
OUTPUT = HERE / "results.json"

EXPECTED_HASHES = {
    "source/dependency/c0048/claim.md": (
        "21f43795bebfc6abe211042b3952f13de3b692abf35400bf9b23a0459a2b3a5e"
    ),
    "source/dependency/c0048/results.json": (
        "f9dec46b07af6604461b5b1bd142be06a8a71f65c24324e54123e4ee81123349"
    ),
    "source/dependency/c0048/verify.py": (
        "6e0aface67cb5cfbb1872f9ab15ed67b0ee1660bae9a02a857982c1a804492f7"
    ),
    "source/primary/axler-2203.05917.tex": (
        "0436439c8c2b8a2c13cc7ef1935cb8d62136ff1784f035da9673f98f4853bfa9"
    ),
    "source/primary/axler-integers-24-A34.pdf": (
        "c093bd507a7e130d1c28ebe8a8707d811a39f8c60ba6cc598afc4bc6e2e522f9"
    ),
    "source/primary/axler-integers-24-A34.txt": (
        "5597897b3fed188cbaee881fb8a0048ecfdcf265edbf2dc1fb69a8787781d50e"
    ),
    "source/primary/buthe-1511.02032.pdf": (
        "350f96313810ded3e8eaf2af6006b227c8834235e177f49eabb3d43d4931c4d1"
    ),
    "source/primary/buthe-1511.02032.txt": (
        "584e158d4e4d3dd3aee1242f94ceaed34f8af77527d4974f1d86519a3178c3c2"
    ),
    "source/primary/fiori-kadiri-swidinsky-2206.12557v2.pdf": (
        "405e5dcbca6067fa436141b8a08c79b81bc12deca03bfe12d667428c36b50fbb"
    ),
    "source/primary/fiori-kadiri-swidinsky-2206.12557v2.txt": (
        "9c926ea1ed333e8008c245f8f5bdd87c72fff0eb1647f87d7e02fbf198169edf"
    ),
    "source/repository/experiment-runner.py": (
        "478ca10db6bde01e6af0d07a0091ff9e3b175bfc4a793c2f7e3d235439b33b82"
    ),
    "source/repository/literature-search.md": (
        "588f211f3f6a49e09e6aaeb08e8d51715e7e664e0e5fa91be283d0c92ebc0a61"
    ),
    "source/repository/original-proof-note.md": (
        "9a49d516c98c5afefb1f4a6899dc58d7c5b9a1799ccba3fff368a09faea68032"
    ),
    "source/repository/original-result.md": (
        "f7ec38edeff5ba5d8542ae10a0fae664de154cc5d73ed95df7714bf300f162e8"
    ),
    "source/repository/original-verify.py": (
        "93b011a137d3ee8b88301e1600c8c9c2f8816e143b1712b4fb17059f337b3c6e"
    ),
    "source/repository/previous-pin.md": (
        "d51281e422db643d674dd7e5017c3c87fb0a38a97631e6d2c392ec5101993d84"
    ),
}

EXPECTED_RUNTIME = {
    "python": "3.14.6",
    "numpy": "2.5.1",
    "python-flint": "0.9.0",
    "flint": "3.6.0",
}
EXPECTED_ORIGINAL_REPORT_HASH = (
    "07ba9371f5d2bad94a7100eeebc2185b56c04c820df2047db5ce0446462ac783"
)

DELTA_Q = Fraction(145_407, 10_000_000)
COEFFICIENTS_Q = (
    None,
    Fraction(1),
    Fraction(1),
    Fraction(2),
    Fraction(6) + DELTA_Q,
    Fraction(24),
    Fraction(120),
    Fraction(720),
    Fraction(30_486, 5),
)
LI_MAJORANT_ORDER = 15
LI_MAJORANT_START = 40
LI_REMAINDER_Q = Fraction(
    2 * factorial(LI_MAJORANT_ORDER + 1) * LI_MAJORANT_START,
    LI_MAJORANT_START - (LI_MAJORANT_ORDER + 2),
)
EXPECTED_ACTIVE_REQUIREMENT_Q = Fraction(
    28_246_867_609_287_917_082_201_314_322_797,
    1_942_607_666_008_652_343_750_000_000_000_000,
)


def require(condition: bool, label: str) -> None:
    if not condition:
        raise RuntimeError(label)


def sha256(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()


def normalized(path: Path) -> str:
    return re.sub(r"\s+", " ", path.read_text(errors="strict"))


def pin_sources() -> dict[str, str]:
    actual = {
        relative: sha256(HERE / relative)
        for relative in sorted(EXPECTED_HASHES)
    }
    require(actual == EXPECTED_HASHES, "source pin mismatch")
    return actual


def pin_runtime() -> dict[str, str]:
    actual = {
        "python": platform.python_version(),
        "numpy": version("numpy"),
        "python-flint": version("python-flint"),
        "flint": flint.__FLINT_VERSION__,
    }
    require(actual == EXPECTED_RUNTIME, f"runtime mismatch: {actual}")
    return actual


def load_original():
    spec = importlib.util.spec_from_file_location("c0050_original", ORIGINAL)
    require(spec is not None and spec.loader is not None, "cannot load original")
    module = importlib.util.module_from_spec(spec)
    spec.loader.exec_module(module)
    return module


def audit_source_anchors() -> dict[str, list[str]]:
    axler = normalized(SOURCE / "primary" / "axler-integers-24-A34.txt")
    buthe = normalized(SOURCE / "primary" / "buthe-1511.02032.txt")
    fks = normalized(
        SOURCE / "primary" / "fiori-kadiri-swidinsky-2206.12557v2.txt"
    )
    anchors = {
        "axler": [
            "Proposition 5. For every x > 1",
            "120.12167x 720.73002x 6098x",
        ],
        "buthe": [
            "li(x) − π(x) > 0 for 2 ≤ x ≤ 1019",
        ],
        "fks": [
            "li(x) − Li(x) = li(2)",
            "Eπ (x) ≤ επ,num (x1 ), for all x ≥ x1",
            "Corollary 22. For all x ≥ 2 we have",
            "0.84768363",
            "Table 4. Values for επ,num",
            "2 000 1.5701 e-12",
            "2 100 1.3254 e-12",
            "Table 7. Other forms of bounds Eπ ≤ B(x)",
        ],
    }
    texts = {"axler": axler, "buthe": buthe, "fks": fks}
    for name, tokens in anchors.items():
        for token in tokens:
            require(token in texts[name], f"{name} missing anchor {token!r}")
    return anchors


def audit_dependency() -> dict[str, object]:
    payload = json.loads(
        (SOURCE / "dependency" / "c0048" / "results.json").read_text()
    )
    require(payload["verdict"] == "ACCEPT", "C-0048 is not accepted")
    coefficients = payload["original_verifier"]["payload"]["coefficients"]
    require(coefficients["fifth"] == "24", "C-0048 fifth mismatch")
    require(coefficients["sixth"] == "120", "C-0048 sixth mismatch")
    require(coefficients["seventh"] == "720", "C-0048 seventh mismatch")
    require(coefficients["eighth"] == "6097.2", "C-0048 eighth mismatch")
    return {
        "claim": "C-0048",
        "verdict": payload["verdict"],
        "coefficients": coefficients,
    }


def audit_exact_derivative(module) -> dict[str, str]:
    require(module.DELTA_Q == DELTA_Q, "delta mismatch")
    require(module.COEFFICIENTS_Q == COEFFICIENTS_Q, "coefficient mismatch")
    derivative = {
        1: COEFFICIENTS_Q[1],
        2: COEFFICIENTS_Q[2] - COEFFICIENTS_Q[1],
        3: COEFFICIENTS_Q[3] - 2 * COEFFICIENTS_Q[2],
        4: COEFFICIENTS_Q[4] - 3 * COEFFICIENTS_Q[3],
        5: COEFFICIENTS_Q[5] - 4 * COEFFICIENTS_Q[4],
        6: COEFFICIENTS_Q[6] - 5 * COEFFICIENTS_Q[5],
        7: COEFFICIENTS_Q[7] - 6 * COEFFICIENTS_Q[6],
        8: COEFFICIENTS_Q[8] - 7 * COEFFICIENTS_Q[7],
        9: -8 * COEFFICIENTS_Q[8],
    }
    expected = {
        1: Fraction(1),
        2: Fraction(0),
        3: Fraction(0),
        4: DELTA_Q,
        5: -4 * DELTA_Q,
        6: Fraction(0),
        7: Fraction(0),
        8: Fraction(5_286, 5),
        9: -Fraction(243_888, 5),
    }
    require(derivative == expected, "derivative identity failed")
    return {str(power): str(value) for power, value in derivative.items()}


def decimal_scientific(mantissa: str, exponent: str) -> Fraction:
    power = int(exponent)
    value = Fraction(mantissa)
    if power >= 0:
        return value * 10**power
    return value / 10 ** (-power)


def parse_fks_table() -> tuple[tuple[int, Fraction], ...]:
    text = (
        SOURCE
        / "primary"
        / "fiori-kadiri-swidinsky-2206.12557v2.txt"
    ).read_text()
    start = text.index("Table 4. Values for")
    end = text.index("Table 5. Sample of values", start)
    table_text = text[start:end]
    pattern = re.compile(
        r"(?<![\d.])(\d{1,3}(?: \d{3})*)\s+"
        r"(\d+\.\d+)\s+e([−-]\d+)"
    )
    rows: list[tuple[int, Fraction]] = []
    artifacts: list[tuple[int, Fraction]] = []
    for log_text, mantissa, exponent in pattern.findall(table_text):
        log_x = int(log_text.replace(" ", ""))
        exponent = exponent.replace("−", "-")
        epsilon = decimal_scientific(mantissa, exponent)
        if (log_x, mantissa, exponent) in {
            (106, "3.8635", "-359"),
            (107, "1.0364", "-1153"),
        }:
            artifacts.append((log_x, epsilon))
            continue
        if 44 <= log_x <= 3_000:
            rows.append((log_x, epsilon))
    result = tuple(sorted(rows))
    require(len(artifacts) == 2, "FKS extraction artifacts changed")
    require(len(result) == 164, "FKS row count mismatch")
    require(len({log_x for log_x, _ in result}) == 164, "duplicate FKS row")
    return result


def literal_table_rows() -> tuple[tuple[int, Fraction], ...]:
    tree = ast.parse(ORIGINAL.read_text())
    assignment = next(
        node
        for node in tree.body
        if isinstance(node, ast.Assign)
        and any(
            isinstance(target, ast.Name) and target.id == "FKS_TABLE_ROWS"
            for target in node.targets
        )
    )

    def convert(node: ast.AST):
        if isinstance(node, ast.Tuple):
            return tuple(convert(element) for element in node.elts)
        if isinstance(node, ast.Constant) and isinstance(node.value, int):
            return node.value
        if (
            isinstance(node, ast.Call)
            and isinstance(node.func, ast.Name)
            and node.func.id == "Fraction"
        ):
            return Fraction(*(convert(argument) for argument in node.args))
        raise RuntimeError(f"unsupported AST node: {ast.dump(node)}")

    rows = convert(assignment.value)
    require(isinstance(rows, tuple), "FKS literal is not a tuple")
    return rows


# Preserve the table API consumed by the C-0055 verifier while sourcing it
# from the hash-pinned original literal rather than duplicating 164 rows.
FKS_TABLE_ROWS = literal_table_rows()


def normalized_remainder_q(log_x: int) -> Fraction:
    log_q = Fraction(log_x)
    value = Fraction(5_286, 5) / log_q**7
    for index in range(8, LI_MAJORANT_ORDER + 1):
        value -= Fraction(factorial(index)) / log_q**index
    value -= LI_REMAINDER_Q / log_q ** (LI_MAJORANT_ORDER + 1)
    return value


def normalized_gap_q(log_x: int) -> Fraction:
    log_q = Fraction(log_x)
    normalized_f = sum(
        COEFFICIENTS_Q[power] / log_q**power
        for power in range(1, 9)
    )
    li_majorant = sum(
        Fraction(factorial(index)) / log_q ** (index + 1)
        for index in range(LI_MAJORANT_ORDER + 1)
    )
    li_majorant += LI_REMAINDER_Q / log_q ** (LI_MAJORANT_ORDER + 2)
    return log_q * (normalized_f - li_majorant)


def audit_fks_table(module) -> dict[str, object]:
    parsed = parse_fks_table()
    literal = literal_table_rows()
    require(parsed == literal, "FKS source transcript differs from AST literal")
    require(parsed == module.FKS_TABLE_ROWS, "loaded FKS rows differ")
    require(parsed[0][0] == 44 and parsed[-1][0] == 3_000, "FKS range")

    requirements = []
    margins = []
    for (left, epsilon), (right, _) in zip(parsed, parsed[1:]):
        requirement = (epsilon - normalized_remainder_q(right)) * right**3
        require(DELTA_Q > requirement, f"FKS reserve failed on {left},{right}")
        requirements.append((requirement, left, right))
        margin = normalized_gap_q(right) - epsilon
        require(margin > 0, f"FKS exact margin failed on {left},{right}")
        margins.append((margin, left, right))

    active_requirement, active_left, active_right = max(requirements)
    require((active_left, active_right) == (2_000, 2_100), "active interval")
    require(
        active_requirement == EXPECTED_ACTIVE_REQUIREMENT_Q,
        "active requirement mismatch",
    )
    minimum_margin, minimum_left, minimum_right = min(margins)
    require((minimum_left, minimum_right) == (2_000, 2_100), "minimum margin")
    return {
        "parsed_rows": len(parsed),
        "source_matches_ast_literal": True,
        "filtered_pdf_text_artifacts": ["10^6 -> 106", "10^7 -> 107"],
        "active_interval": [active_left, active_right],
        "active_requirement_exact": str(active_requirement),
        "delta_minus_requirement_exact": str(DELTA_Q - active_requirement),
        "minimum_exact_margin": str(minimum_margin),
    }


def audit_finite_boundaries(module) -> dict[str, object]:
    sieve = module.odd_sieve(module.SPLIT)
    odd_indices = module.np.flatnonzero(
        module.np.frombuffer(sieve, dtype=module.np.uint8)
    )
    total = 1 + int(odd_indices.size)
    require(total == module.PI_SPLIT == 55_662_470, "split prime count mismatch")
    for endpoint, expected in (
        (10, 4),
        (100, 25),
        (1_000, 168),
        (1_000_000, 78_498),
    ):
        last_odd_index = (endpoint - 1) // 2
        odd_count = int(
            module.np.searchsorted(odd_indices, last_odd_index, side="right")
        )
        require(1 + odd_count == expected, f"prime count fixture {endpoint}")

    covered = 14
    blocks = 0
    first = None
    last = None
    minimum = None
    while covered < total:
        start_count = covered + 1
        start_prime = 2 * int(odd_indices[start_count - 2]) + 1
        first = first or (start_count, start_prime)
        last = (start_count, start_prime)
        value = module.prime_bound(start_prime)
        target = min(total, math.floor(float(value.lower()) - 0.25))
        while not value > target:
            target -= 1
        require(target >= start_count, "empty finite block")
        slack = value - target
        require(slack > module.q(Fraction(1, 4)), "slack not above 1/4")
        minimum = (
            slack
            if minimum is None or slack.lower() < minimum.lower()
            else minimum
        )
        if target < total:
            next_prime = 2 * int(odd_indices[target - 1]) + 1
            require(next_prime > start_prime, "bad next-prime boundary")
        covered = target
        blocks += 1

    require(first == (15, 47), "first block is not p_15")
    require(covered == total, "finite cover does not reach split")
    require(blocks == 58_006, "unexpected block count")
    return {
        "prime_count": total,
        "blocks": blocks,
        "first_start": list(first),
        "last_start": list(last),
        "minimum_block_slack": str(minimum),
    }


def audit_original_functions(module) -> dict[str, object]:
    module.verify_derivative_identity()
    small = module.verify_small_range()
    monotonicity = module.verify_monotonicity()
    li_bridge = module.verify_li_bridge()
    majorant = module.verify_li_ratio_majorant()
    tail = module.verify_fks_tail()
    require(arb(small) > 15, "small-range minimum failed")
    require(arb(monotonicity) > 3_500, "monotonicity failed")
    require(arb(li_bridge["gap_at_split"]) > arb("0.428"), "li bridge failed")
    require(
        arb(majorant["gap_derivative_factor"]) < 0,
        "normalized gap is not decreasing",
    )
    require(arb(tail["table7_margin"]) > 0, "Table 7 margin failed")
    require(
        arb(tail["table4"]["minimum_interval_margin"]) > 0,
        "Table 4 margin failed",
    )
    require(
        arb(tail["asymptotic"]["margin_at_log_3000"]) > 0,
        "Corollary 22 handoff failed",
    )
    return {
        "small_range": small,
        "monotonicity": monotonicity,
        "li_bridge": li_bridge,
        "li_ratio_majorant": majorant,
        "fks_tail": tail,
    }


def run_original() -> dict[str, object]:
    completed = subprocess.run(
        [sys.executable, str(ORIGINAL)],
        check=True,
        capture_output=True,
        text=True,
    )
    require(completed.stdout.rstrip().endswith("PASS"), "original did not pass")
    digest = hashlib.sha256(completed.stdout.encode()).hexdigest()
    require(digest == EXPECTED_ORIGINAL_REPORT_HASH, "original output drift")
    payload = json.loads(completed.stdout.rsplit("\nPASS", 1)[0])
    require(payload["coefficients"]["fourth"] == "6.0145407", "fourth mismatch")
    require(payload["finite_cover"]["blocks"] == 58_006, "block count mismatch")
    require(
        arb(payload["finite_cover"]["minimum_block_slack"]) > arb("0.25"),
        "reported finite slack is too small",
    )
    require(
        payload["fks_tail"]["table4"]["active_interval"] == [2_000, 2_100],
        "reported active interval mismatch",
    )
    return {
        "payload": payload,
        "stdout_sha256": digest,
    }


def audit_previous_certificate_defect() -> str:
    source = ORIGINAL.read_text()
    require("assert " in source, "original verifier did not use assertions")
    require("if not __debug__" not in source, "original already rejects -O")
    return (
        "previous canonical verifier used bare assert without rejecting "
        "optimized Python and omitted the primary-source files it cited"
    )


def main() -> None:
    module = load_original()
    result = {
        "verdict": "ACCEPT",
        "claim": "C-0050",
        "material_defect_repaired": audit_previous_certificate_defect(),
        "source_hashes": pin_sources(),
        "source_anchors": audit_source_anchors(),
        "runtime": pin_runtime(),
        "dependency": audit_dependency(),
        "exact_derivative": audit_exact_derivative(module),
        "fks_table_transcript": audit_fks_table(module),
        "finite_boundary_audit": audit_finite_boundaries(module),
        "independent_function_audit": audit_original_functions(module),
        "original_verifier": run_original(),
        "normalization": (
            "FKS uses signed E_pi=(pi-Li)/(x/log x); since "
            "li-Li=li(2)>0, F-Li is strictly larger than F-li"
        ),
        "scope": "explicit prime-counting inequality only; all-height RH excluded",
    }
    OUTPUT.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()
