#!/usr/bin/env python3
"""Exhaustive causal-prefix GCD checker for the cyclic two-hinge carrier.

An update x=(p,A) acts as T_x(S)=A union p(S).  If prefix x is followed by
continuation y, the composite is T_y o T_x.  For the transitive cyclic
two-hinge carriers, equality of all such future Look rows identifies prefixes
exactly by their opened-site mask A (the prefix permutation is unobservable).

A semantic prefix factor with mask A divides a target with mask C iff some
hinge-group translate of A is contained in C.  The checker enumerates common
factors of every target pair and finds the first pair having nonassociated
maximal common factors.
"""

from __future__ import annotations

import argparse
import itertools
import json
from pathlib import Path


def compose_perm(p, q):
    return tuple(p[q[i]] for i in range(len(p)))


def image_mask(p, mask):
    out = 0
    for i, j in enumerate(p):
        if mask >> i & 1:
            out |= 1 << j
    return out


def generators(n):
    return (
        tuple((-i) % n for i in range(n)),
        tuple((2 - i) % n for i in range(n)),
    )


def generated_group(n):
    ident = tuple(range(n))
    group = {ident}
    todo = [ident]
    while todo:
        p = todo.pop()
        for g in generators(n):
            h = compose_perm(p, g)
            if h not in group:
                group.add(h)
                todo.append(h)
    return tuple(sorted(group))


def orbit(mask, group):
    return frozenset(image_mask(p, mask) for p in group)


def divides(pattern, target, group):
    return any((moved & ~target) == 0 for moved in orbit(pattern, group))


def associated(a, b, group):
    return b in orbit(a, group)


def maximal_common_factors(a, b, n, group):
    common = [
        d for d in range(1 << n)
        if divides(d, a, group) and divides(d, b, group)
    ]
    return [
        d for d in common
        if not any(
            d != e
            and divides(d, e, group)
            and not divides(e, d, group)
            for e in common
        )
    ]


def search_n(n):
    group = generated_group(n)
    masks = range(1 << n)
    witness = None
    pairs_checked = 0
    for a in masks:
        for b in range(a, 1 << n):
            pairs_checked += 1
            maximal = maximal_common_factors(a, b, n, group)
            bad = next(
                (
                    (d, e)
                    for d, e in itertools.combinations(maximal, 2)
                    if not associated(d, e, group)
                ),
                None,
            )
            if bad:
                witness = {
                    "target_masks": [a, b],
                    "nonassociated_maximal_factor_masks": list(bad),
                    "all_maximal_factor_masks": maximal,
                }
                break
        if witness:
            break
    return {
        "n": n,
        "group_order": len(group),
        "target_pairs_checked_until_first_failure_or_exhaustion": pairs_checked,
        "witness": witness,
    }


def verify_pentagon():
    n = 5
    group = generated_group(n)
    c1 = 0b00111       # {0,1,2}
    c2 = 0b01011       # {0,1,3}
    edge = 0b00011     # {0,1}
    diagonal = 0b00101 # {0,2}
    assert divides(edge, c1, group) and divides(edge, c2, group)
    assert divides(diagonal, c1, group) and divides(diagonal, c2, group)
    assert not associated(edge, diagonal, group)
    assert not associated(c1, c2, group)
    maximal = maximal_common_factors(c1, c2, n, group)
    assert edge in maximal and diagonal in maximal
    assert all(m.bit_count() == 2 for m in maximal)
    return {
        "targets": [c1, c2],
        "target_orbits": "complements are diagonal versus edge",
        "maximal_common_factor_representatives": [edge, diagonal],
        "factor_orbits": "edge versus diagonal",
        "verified": True,
    }


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("--max-n", type=int, default=5)
    parser.add_argument("--certificate", type=Path)
    args = parser.parse_args()
    rows = [search_n(n) for n in range(1, args.max_n + 1)]
    cert = {
        "model": "causal full-future cyclic two-hinge Boolean carrier",
        "status": "verified",
        "explicit_pentagon_certificate": verify_pentagon(),
        "census": rows,
        "first_failure_n": next(
            (row["n"] for row in rows if row["witness"]),
            None,
        ),
    }
    text = json.dumps(cert, indent=2) + "\n"
    if args.certificate:
        args.certificate.write_text(text)
    print(text, end="")


if __name__ == "__main__":
    main()