#!/usr/bin/env python3
"""Exhaustive checker for the finite Boolean two-hinge update algebra.

Carrier: Z/nZ.
Hinges: the involutions r0(i)=-i and r1(i)=2-i (mod n).
Sites: a Boolean hole mask A.  Writing is append-only: x -> x union A.
Motion/update element: (p,A), acting as x -> p(x) union A, where p belongs
to the permutation group generated by r0,r1.
Composition: (p,A)*(q,B)=(p q, A union p(B)).

The final physical fibers are the orbits of <r0,r1>.  Look is OR over
fibers of AND over the sites in that fiber.
"""

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):
    ans = 0
    for i, j in enumerate(p):
        if mask >> i & 1:
            ans |= 1 << j
    return ans


def mul(x, y):
    p, a = x
    q, b = y
    return compose_perm(p, q), a | image_mask(p, b)


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))
    gens = generators(n)
    group = {ident}
    todo = [ident]
    while todo:
        p = todo.pop()
        for g in gens:
            h = compose_perm(p, g)
            if h not in group:
                group.add(h)
                todo.append(h)
    return tuple(sorted(group))


def inverse(p):
    ans = [0] * len(p)
    for i, j in enumerate(p):
        ans[j] = i
    return tuple(ans)


def left_residual(d, v):
    """Construct a residual q with v=d*q, or return None."""
    p, a = d
    q, b = v
    if a & ~b:
        return None
    pinv = inverse(p)
    residual = (compose_perm(pinv, q), image_mask(pinv, b & ~a))
    assert mul(d, residual) == v
    return residual


def left_divides(d, v, _group=None):
    return left_residual(d, v) is not None


def canonical_gcd(vector, ident):
    common_mask = (1 << len(ident)) - 1
    for _, mask in vector:
        common_mask &= mask
    return ident, common_mask


def right_associate(x, y, group):
    """x and y differ by multiplication on the right by a unit."""
    units = ((p, 0) for p in group)
    return any(mul(x, u) == y for u in units)


def fibers(n):
    gens = generators(n)
    unseen = set(range(n))
    ans = []
    while unseen:
        root = min(unseen)
        orbit = {root}
        todo = [root]
        while todo:
            i = todo.pop()
            for g in gens:
                j = g[i]
                if j not in orbit:
                    orbit.add(j)
                    todo.append(j)
        unseen -= orbit
        ans.append(tuple(sorted(orbit)))
    return tuple(ans)


def look(mask, partition):
    return int(any(all(mask >> i & 1 for i in block) for block in partition))


def activation_vector(mask, partition):
    return tuple(
        int(all(mask >> i & 1 for i in block))
        for block in partition
    )


def future_activation_profile(mask, partition, n):
    """All labelled fiber-activation rows after every append-only mask."""
    return tuple(
        activation_vector(mask | extension, partition)
        for extension in range(1 << n)
    )


def future_look_profile(mask, partition, n):
    """All final Look bits after every append-only mask."""
    return tuple(
        look(mask | extension, partition)
        for extension in range(1 << n)
    )


def verify_n(n, vector_arity, exhaustive_limit):
    group = generated_group(n)
    ident = tuple(range(n))
    elems = tuple((p, a) for p in group for a in range(1 << n))
    vectors = itertools.product(elems, repeat=vector_arity)
    checked = 0
    for vector in vectors:
        checked += 1
        if exhaustive_limit and checked > exhaustive_limit:
            break
        gcd = canonical_gcd(vector, ident)
        assert all(left_divides(gcd, v, group) for v in vector)
        common = [d for d in elems if all(left_divides(d, v, group) for v in vector)]
        maximal = [
            d for d in common
            if not any(d != e and left_divides(d, e, group) and
                       not left_divides(e, d, group) for e in common)
        ]
        assert maximal
        assert all(right_associate(gcd, d, group) for d in maximal)
        # Exact characterization: common left factors have mask contained
        # in the intersection mask.
        intersection = gcd[1]
        assert all((d[1] & ~intersection) == 0 for d in common)
        assert len(common) == len(group) * (1 << intersection.bit_count())

    part = fibers(n)
    rows = {}
    for mask in range(1 << n):
        rows.setdefault(look(mask, part), []).append(mask)
    collision = next(
        ((a, b) for bucket in rows.values() for a, b in itertools.combinations(bucket, 2)
         if a != b),
        None,
    )
    distinguishing_append = None
    if collision:
        a, b = collision
        distinguishing_append = next(
            (
                c
                for c in range(1 << n)
                if look(a | c, part) != look(b | c, part)
            ),
            None,
        )
    activation_profiles = {
        mask: future_activation_profile(mask, part, n)
        for mask in range(1 << n)
    }
    assert len(set(activation_profiles.values())) == 1 << n

    look_profiles = {
        mask: future_look_profile(mask, part, n)
        for mask in range(1 << n)
    }
    accepting = {mask for mask in range(1 << n) if look(mask, part)}
    for a, b in itertools.product(range(1 << n), repeat=2):
        same_expected = a == b or (a in accepting and b in accepting)
        assert (look_profiles[a] == look_profiles[b]) == same_expected
    future_look_collision = next(
        (
            (a, b)
            for a, b in itertools.combinations(range(1 << n), 2)
            if look_profiles[a] == look_profiles[b]
        ),
        None,
    )
    return {
        "n": n,
        "hinges": [list(x) for x in generators(n)],
        "group_order": len(group),
        "element_count": len(elems),
        "fiber_partition": [list(x) for x in part],
        "vectors_checked": min(checked, exhaustive_limit or checked),
        "vector_arity": vector_arity,
        "gcd_rule": "identity permutation plus intersection of target write masks",
        "maximal_common_factors_unique_up_to_right_units": True,
        "look_collision": list(collision) if collision else None,
        "look_collision_values": [look(collision[0], part), look(collision[1], part)]
        if collision else None,
        "shortest_distinguishing_append_mask": distinguishing_append,
        "post_append_look_values": [
            look(collision[0] | distinguishing_append, part),
            look(collision[1] | distinguishing_append, part),
        ]
        if collision and distinguishing_append is not None
        else None,
        "future_labelled_activation_profile_is_injective": True,
        "future_look_kernel":
            "equality on nonaccepting masks; one class containing every accepting mask",
        "future_look_collision": list(future_look_collision)
        if future_look_collision else None,
    }


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--max-n", type=int, default=4)
    ap.add_argument("--arity", type=int, default=2)
    ap.add_argument("--limit", type=int, default=0,
                    help="vectors per n; zero means exhaustive")
    ap.add_argument("--certificate", type=Path)
    args = ap.parse_args()
    results = [verify_n(n, args.arity, args.limit) for n in range(1, args.max_n + 1)]
    cert = {
        "model": "finite Boolean two-hinge append/permutation update algebra",
        "status": "verified",
        "results": results,
    }
    if args.certificate:
        args.certificate.write_text(json.dumps(cert, indent=2) + "\n")
    print(json.dumps(cert, indent=2))


if __name__ == "__main__":
    main()