#!/usr/bin/env python3
"""Dependency-free hostile synthesis verifier for C-0065."""

from __future__ import annotations

import hashlib
import subprocess
import sys
from collections import defaultdict
from fractions import Fraction
from itertools import combinations, permutations
from math import factorial
from pathlib import Path


def repository_root(path: Path) -> Path:
    for parent in path.parents:
        if (parent / "bin" / "rhc.py").is_file():
            return parent
    raise RuntimeError("repository root not found")


ROOT = repository_root(Path(__file__).resolve())
DEPENDENCIES = {
    "canon/claims/C-0043-sharp-degree-thirteen-karlin-wronskian.md":
        "162037365509a25e68b2b2a94a531fbdfac519a29fa074df09dc5011fcd1a67e",
    "canon/witnesses/C-0043/verify.py":
        "d2c81bc63eff8cb1b5ddd0dc1668791a0ee098b5c0355607fdf0d44dc53c1b08",
    "canon/claims/C-0056-sharp-degree-eight-karlin-wronskian.md":
        "1140f45188b8d3ccd4716d7aed8dbc0d65f66547deb6fcc702189a4180d5398a",
    "canon/witnesses/C-0056/verify.py":
        "4d5a17fea7113c4a0dead5c3218eb267e090bc7fb6139fe8a12216cf310c709e",
    "canon/claims/C-0059-sharp-degree-seven-signed-karlin-wronskian.md":
        "266942aeaf2ced98f3c8527743b2a8985ebe7d9e7e0c4cc91b04213cd742b111",
    "canon/witnesses/C-0059/verify.py":
        "e1dd49b2ec5d26b121d16c2055e93ab5146c5f58cd4fcd3fa8f0dd2671fce395",
}
DEPENDENCY_VERIFIERS = (
    "canon/witnesses/C-0043/verify.py",
    "canon/witnesses/C-0056/verify.py",
    "canon/witnesses/C-0059/verify.py",
)
EXPECTED_BOUNDARY = -1_246_946_918_400
EXPECTED_SIMPLE_SHA256 = (
    "3cee62a7790b6341ed2b586e6cf3dd0add9e3e9499bca2116bc1846f2569c5ca"
)
EXPECTED_SOURCE_SHA256 = {
    "cc2002-page16.png":
        "6c7b50158ff09e43285c05ad6e3ecead08c8b708d2bd624d2e4d33884713438f",
    "cc2002-page17.png":
        "bf1e3c33ab0130949222ab1ad6b445d9c07f4ffa1a864926c68c5977dcc4a993",
    "cc2005-page64.png":
        "96eb61475e398a8150f0cd681f4d36b888c4485be99aabbfa6308c6e907afbec",
    "cc2005-page67.png":
        "6413d21d1938a751cacd93b3552fde39270099c5c501a5ec790acc09d7b9d4b7",
    "cc2005-page68.png":
        "de8e54c4fc8b7451906b7a7b90c9173bd8cc117a5cce6bb9009be8cb2689ccb9",
    "craven-csordas-2002-iterated-laguerre-turan.pdf":
        "945310b929c47aee17cbc5f0a8bf3fb25cd6c52f14da88c5117dd9bed3b59714",
    "craven-csordas-2002-iterated-laguerre-turan.txt":
        "db7f2cda0b0e3ca995c42f7854dbeaa4c4940368dce2e357821c3eeb4e04a318",
    "craven-csordas-2005-karlin-conjecture.pdf":
        "bd9fc2f503621a371c2cbda72a7130df5ba2ba56b776260d865ed96f2e6c6746",
    "craven-csordas-2005-karlin-conjecture.txt":
        "49603f4dd6fe6e5c3da0fe84004b3512476d9b3d244258a3f1934b946499dac9",
    "original-verify.py":
        "024440e30f6fd292fc9c50e9ff6714d8c2f89a405893412f79e5eb5f64a64d46",
}

Exponent = tuple[int, ...]
Polynomial = dict[Exponent, int]


if not __debug__:
    raise SystemExit("verify.py requires assertions")


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


def add(left: Polynomial, right: Polynomial) -> Polynomial:
    result: defaultdict[Exponent, int] = defaultdict(int)
    for exponents, coefficient in left.items():
        result[exponents] += coefficient
    for exponents, coefficient in right.items():
        result[exponents] += coefficient
    return {key: value for key, value in result.items() if value}


def scale(polynomial: Polynomial, scalar: int) -> Polynomial:
    return {
        exponents: scalar * coefficient
        for exponents, coefficient in polynomial.items()
        if scalar * coefficient
    }


def multiply(left: Polynomial, right: Polynomial) -> Polynomial:
    result: defaultdict[Exponent, int] = defaultdict(int)
    for left_exp, left_coefficient in left.items():
        for right_exp, right_coefficient in right.items():
            exponents = tuple(
                a + b
                for a, b in zip(left_exp, right_exp, strict=True)
            )
            result[exponents] += left_coefficient * right_coefficient
    return {key: value for key, value in result.items() if value}


def permutation_sign(permutation: tuple[int, ...]) -> int:
    inversions = sum(
        permutation[i] > permutation[j]
        for i in range(len(permutation))
        for j in range(i + 1, len(permutation))
    )
    return -1 if inversions % 2 else 1


def polynomial_determinant(matrix: list[list[Polynomial]]) -> Polynomial:
    variables = len(next(iter(next(cell for row in matrix for cell in row if cell))))
    one = {(0,) * variables: 1}
    result: Polynomial = {}
    for permutation in permutations(range(len(matrix))):
        term = one
        for row, column in enumerate(permutation):
            term = multiply(term, matrix[row][column])
            if not term:
                break
        result = add(result, scale(term, permutation_sign(permutation)))
    return result


def elementary_polynomials(variables: int) -> list[Polynomial]:
    result = []
    for degree in range(variables + 1):
        polynomial = {}
        for subset in combinations(range(variables), degree):
            exponents = [0] * variables
            for index in subset:
                exponents[index] = 1
            polynomial[tuple(exponents)] = 1
        result.append(polynomial)
    return result


def power_sum(variables: int, degree: int) -> Polynomial:
    result = {}
    for index in range(variables):
        exponents = [0] * variables
        exponents[index] = degree
        result[tuple(exponents)] = 1
    return result


def verify_low_ranks() -> None:
    variables = 6
    elementary = elementary_polynomials(variables)
    derivatives = [
        scale(elementary[degree], factorial(degree))
        for degree in range(5)
    ]
    rank_two = scale(
        polynomial_determinant(
            [[derivatives[0], derivatives[1]],
             [derivatives[1], derivatives[2]]]
        ),
        -1,
    )
    assert rank_two == power_sum(variables, 2)

    rank_three = scale(
        polynomial_determinant(
            [
                [derivatives[0], derivatives[1], derivatives[2]],
                [derivatives[1], derivatives[2], derivatives[3]],
                [derivatives[2], derivatives[3], derivatives[4]],
            ]
        ),
        -1,
    )
    p2 = power_sum(variables, 2)
    p3 = power_sum(variables, 3)
    p4 = power_sum(variables, 4)
    power_formula = scale(
        add(
            add(multiply(multiply(p2, p2), p2), scale(multiply(p2, p4), -3)),
            scale(multiply(p3, p3), 2),
        ),
        2,
    )
    positive: Polynomial = {}
    for left, right in combinations(range(variables), 2):
        exponents = [0] * variables
        exponents[left] = exponents[right] = 3
        positive[tuple(exponents)] = 8
    for subset in combinations(range(variables), 3):
        exponents = [0] * variables
        for index in subset:
            exponents[index] = 2
        positive[tuple(exponents)] = 12
    assert rank_three == power_formula == positive
    assert all(coefficient > 0 for coefficient in positive.values())


def verify_high_ranks() -> None:
    degree = 6
    admissible = [
        permutation
        for permutation in permutations(range(7))
        if all(row + column <= degree for row, column in enumerate(permutation))
    ]
    reversal = tuple(reversed(range(7)))
    assert admissible == [reversal]
    assert permutation_sign(reversal) == -1
    assert (-1) ** (7 * 6 // 2) == -1
    assert permutation_sign(reversal) * (-1) == 1
    assert factorial(6) ** 7 == 720**7
    for rank in range(8, 40):
        assert rank - 1 > degree
    assert all(rank - 1 > degree for rank in range(8, 10_000))


def product(values):
    result = 1
    for value in values:
        result *= value
    return result


def scalar_determinant(matrix):
    return sum(
        permutation_sign(permutation)
        * product(matrix[row][column] for row, column in enumerate(permutation))
        for permutation in permutations(range(len(matrix)))
    )


def elementary_values(values: tuple[Fraction, ...]) -> list[Fraction]:
    result = [Fraction(1)] + [Fraction(0)] * len(values)
    for value in values:
        for degree in range(len(values), 0, -1):
            result[degree] += value * result[degree - 1]
    return result


def signed_centered(values: tuple[Fraction, ...], rank: int) -> Fraction:
    elementary = elementary_values(values)
    derivatives = [
        factorial(degree) * (
            elementary[degree] if degree < len(elementary) else 0
        )
        for degree in range(2 * rank - 1)
    ]
    determinant = scalar_determinant(
        [
            [derivatives[row + column] for column in range(rank)]
            for row in range(rank)
        ]
    )
    return Fraction((-1) ** (rank * (rank - 1) // 2) * determinant)


def verify_sharpness() -> None:
    coefficients = (0, 0, 0, 0, 1, 3, 3, 1)
    derivatives = [
        factorial(degree) * (
            coefficients[degree] if degree < len(coefficients) else 0
        )
        for degree in range(11)
    ]
    boundary = scalar_determinant(
        [
            [derivatives[row + column] for column in range(6)]
            for row in range(6)
        ]
    )
    assert -boundary == EXPECTED_BOUNDARY

    denominator = 10_000_000
    numerators = (
        53 * denominator - 3,
        53 * denominator - 1,
        53 * denominator + 1,
        53 * denominator + 3,
        denominator - 2,
        denominator,
        denominator + 2,
    )
    roots = tuple(Fraction(numerator, denominator) for numerator in numerators)
    assert len(set(roots)) == 7 and min(roots) > 0
    determinant = signed_centered(roots, 6)
    payload = f"{determinant.numerator}/{determinant.denominator}".encode()
    assert hashlib.sha256(payload).hexdigest() == EXPECTED_SIMPLE_SHA256
    assert determinant < 0


def verify_sources() -> None:
    source_dir = Path(__file__).resolve().parent / "source"
    assert {path.name for path in source_dir.iterdir()} == set(
        EXPECTED_SOURCE_SHA256
    )
    for name, expected in EXPECTED_SOURCE_SHA256.items():
        assert sha256(source_dir / name) == expected
    text = (
        source_dir / "craven-csordas-2005-karlin-conjecture.txt"
    ).read_text()
    assert "(1.7)   (−1)n(n+1)/2 W (f (x), f" in text
    assert "C0 := f (x) =" in text
    assert "Theorem 4.5." in text
    assert "Then the 5 × 5 Wronskian" in text


def verify_dependencies() -> None:
    for relative, expected in DEPENDENCIES.items():
        assert sha256(ROOT / relative) == expected
    for relative in DEPENDENCY_VERIFIERS:
        completed = subprocess.run(
            [sys.executable, str(ROOT / relative)],
            cwd=ROOT,
            capture_output=True,
            text=True,
            check=False,
        )
        assert completed.returncode == 0, completed.stderr
        assert "PASS" in completed.stdout


def main() -> None:
    verify_sources()
    verify_dependencies()
    verify_low_ranks()
    verify_high_ranks()
    verify_sharpness()
    print("primary-source sign and special-class scope: PASS")
    print("C-0043, C-0056, and C-0059 pins and verifiers: PASS")
    print("ranks one through three exact positive formulas: PASS")
    print("rank-seven unique reversal permutation: PASS")
    print("all ranks eight and higher zero-column exhaustion: PASS")
    print("degree-seven boundary and simple-root counterfeits: PASS")


if __name__ == "__main__":
    main()
