check_late_profile_correction.py

#!/usr/bin/env python3
"""Finite semantic diagnostics for run139; not a native timing implementation."""
from itertools import product
import json


def defect(edges, profiles, width):
    # Independent ordered mismatch witnesses, without cell-count arithmetic.
    return sum((v, w) in edges and (x, w) not in edges
               for v in range(len(profiles)) for x in range(len(profiles))
               if profiles[v] == profiles[x] for w in range(width))


def cells(edges, profiles, width, colors):
    H = [profiles.count(m) for m in range(colors)]
    c = [[sum((v, w) in edges and profiles[v] == m
              for v in range(len(profiles))) for m in range(colors)]
         for w in range(width)]
    return H, c


def delta(edges, profiles, width, colors, v, q):
    H, c = cells(edges, profiles, width, colors)
    p = profiles[v]
    ep, eq = sum(row[p] for row in c), sum(row[q] for row in c)
    neighbors = [w for w in range(width) if (v, w) in edges]
    return eq - ep + (H[q] - H[p]) * len(neighbors) + 2 * sum(
        c[w][p] - c[w][q] for w in neighbors)


def masks(edges, profiles, width):
    return tuple(frozenset(profiles[v] for v in range(len(profiles))
                           if (v, w) in edges) for w in range(width))


def main():
    changes = matrices = 0
    collision = {}
    found = None
    width, rows, colors = 3, 3, 3
    for bits in product((0, 1), repeat=rows * width):
        edges = frozenset((v, w) for v in range(rows) for w in range(width)
                          if bits[v * width + w])
        for profiles in product(range(colors), repeat=rows):
            H, c = cells(edges, profiles, width, colors)
            old = defect(edges, profiles, width)
            assert old == sum(cw[m] * (H[m] - cw[m])
                              for cw in c for m in range(colors))
            assert (old == 0) == all(len({(v, w) in edges for v in range(rows)
                                         if profiles[v] == m}) <= 1
                                    for w in range(width) for m in range(colors))
            matrices += 1
            for v in range(rows):
                for q in range(colors):
                    if q == profiles[v]:
                        continue
                    revised = list(profiles)
                    revised[v] = q
                    actual = defect(edges, revised, width) - old
                    assert actual == delta(edges, profiles, width, colors, v, q)
                    changes += 1
                    # Demonstrate insufficiency of the scalar margins alone.
                    p = profiles[v]
                    key = (tuple(H), p, q, sum(row[p] for row in c),
                           sum(row[q] for row in c),
                           sum((v, w) in edges for w in range(width)), old)
                    if key in collision and collision[key][0] != actual:
                        found = (key, collision[key], (actual, tuple(sorted(edges)), profiles, v))
                    else:
                        collision[key] = (actual, tuple(sorted(edges)), profiles, v)
    assert found is not None
    # Before the late move, two target kinds have identical masks. Afterward,
    # the complete kind keeps both profiles; the partial kind loses profile1.
    for size in range(1, 65):
        profiles = (1, 1, 3)  # v,x,y, with anchors A and B
        edges = frozenset((row, w) for w in range(2 * size)
                          for row in ((0, 1, 2) if w % 2 == 0 else (0, 2)))
        before = masks(edges, profiles, 2 * size)
        after = masks(edges, (3, 1, 3), 2 * size)
        assert len(set(before)) == 1 and len(set(after)) == 2
        assert sum(a != b for a, b in zip(before, after)) == size
        assert defect(edges, (3, 1, 3), 2 * size) == 0
        assert defect(edges, profiles, 2 * size) == size
    # Independent event schedules: k=2 anchor bits and two ordinary edges.
    # Count repairs on already inserted edges; each edge is visited at most k.
    from itertools import permutations
    schedules = 0
    for order in permutations(('a', 'b', 'e0', 'e1')):
        present, visits = set(), {'e0': 0, 'e1': 0}
        for event in order:
            if event.startswith('e'):
                present.add(event)
            else:
                for edge in present:
                    visits[edge] += 1
        assert sum(visits.values()) <= 2 * 2
        assert max(visits.values()) <= 2
        schedules += 1
    print(json.dumps({'cell_oracles': matrices, 'profile_moves': changes,
                      'late_split_families': 64, 'repair_schedules': schedules,
                      'scalar_collision': found,
                      'native_timing_evidence': False}, indent=2))


if __name__ == '__main__':
    main()