verify_grid_closure.py

#!/usr/bin/env python3
"""Small exact checks for grid closure and persistent partial assignments.
Python tuples model immutable nodes. This is not a local-machine timing test.
"""
import itertools as it
import json
import random


def edges(m):
    return [(r*m+c, r*m+c+1) for r in range(m) for c in range(m-1)] + [
        (r*m+c, (r+1)*m+c) for r in range(m-1) for c in range(m)]


def independent_cross_matching(es, prefix, b):
    adj = [set() for _ in range(b)]
    for u, v in es:
        adj[u].add(v); adj[v].add(u)
    remaining = [(u, v) if u in prefix else (v, u) for u, v in es
                 if (u in prefix) != (v in prefix)]
    chosen = []
    while remaining:
        u, v = remaining[0]
        chosen.append((u, v))
        forbidden = {u, v} | adj[u] | adj[v]
        remaining = [(a, z) for a, z in remaining if a not in forbidden and z not in forbidden]
    return chosen


def check_cuts(m):
    b, es = m*m, edges(m)
    minimum = 1 << b
    count = 0
    for p in it.combinations(range(b), b//2):
        prefix = set(p)
        suffix = [v for v in range(b) if v not in prefix]
        crossing = sum((u in prefix) != (v in prefix) for u, v in es)
        assert crossing * 3 >= m
        matching = independent_cross_matching(es, prefix, b)
        assert len(matching) * 40 >= crossing
        residuals = set()
        for values in it.product((0, 1), repeat=len(p)):
            a = dict(zip(p, values))
            result = 0
            for j, rest in enumerate(it.product((0, 1), repeat=len(suffix))):
                x = a | dict(zip(suffix, rest))
                result |= int(all(x[u] or x[v] for u, v in es)) << j
            residuals.add(result)
        assert len(residuals) >= 2 ** len(matching)
        minimum = min(minimum, len(residuals))
        count += 1
    return {'m': m, 'balanced_cuts': count, 'minimum_distinct_residuals': minimum}


class Trees:
    def __init__(self, ell):
        self.ell, self.allocations = ell, 0

    def node(self, left, right, value):
        self.allocations += 1
        return (left, right, value)

    def build(self, depth, value):
        if depth == 0:
            return self.node(None, None, value)
        return self.node(self.build(depth-1, value), self.build(depth-1, value), bool(value) if value is not None else None)

    def get(self, root, key):
        for bit in key:
            root = root[bit]
        return root[2]

    def put(self, root, key, value, aggregate=False):
        if not key:
            return self.node(None, None, value)
        bit, rest = key[0], key[1:]
        children = [root[0], root[1]]
        children[bit] = self.put(children[bit], rest, value, aggregate)
        return self.node(*children, (children[0][2] or children[1][2]) if aggregate else None)


def persistent_checks(m, trials=250):
    b, es = m*m, edges(m)
    ell = max(1, (b-1).bit_length())
    keys = [tuple(int(c) for c in format(v, f'0{ell}b')) for v in range(b)]
    incident = [[] for _ in range(b)]
    horizontal, vertical = {}, {}
    for u, v in es:
        group = 0 if v == u+1 else 1
        (horizontal if group == 0 else vertical)[u] = v
        incident[u].append((group, u, v)); incident[v].append((group, u, v))
    tr = Trees(ell)
    assignment = tr.build(ell, None)
    flags = (tr.build(ell, False), tr.build(ell, False))
    versions = [(assignment, flags, (None,)*b)]
    rng = random.Random(9200+m)
    max_nodes = 0
    for _ in range(trials):
        root, flagroots, oracle = rng.choice(versions)
        v, value = rng.randrange(b), rng.choice((None, 0, 1))
        before = tr.allocations
        newroot = tr.put(root, keys[v], value)
        newflags = list(flagroots)
        for group, u, w in incident[v]:
            bad = tr.get(newroot, keys[u]) == 0 and tr.get(newroot, keys[w]) == 0
            newflags[group] = tr.put(newflags[group], keys[u], bad, True)
        allocated = tr.allocations-before
        assert allocated <= 5*(ell+1)
        max_nodes = max(max_nodes, allocated)
        neworacle = list(oracle); neworacle[v] = value
        versions.append((newroot, tuple(newflags), tuple(neworacle)))
        # Recheck every retained version; no old updates may be lost or overwritten.
        for r, f, a in versions:
            assert tuple(tr.get(r, keys[x]) for x in range(b)) == a
            expected = not any(a[u] == 0 and a[w] == 0 for u, w in es)
            assert (not (f[0][2] or f[1][2])) == expected
            completed = [1 if x is None else x for x in a]
            assert expected == all(completed[u] or completed[w] for u, w in es)
    return {'m': m, 'updates': trials, 'retained_versions': len(versions),
            'max_new_tree_nodes_per_update': max_nodes, 'node_bound': 5*(ell+1)}


if __name__ == '__main__':
    print(json.dumps({'cuts': [check_cuts(m) for m in (2, 3)],
                      'persistent': [persistent_checks(m) for m in (2, 3, 5)],
                      'passed': True, 'status': 'finite exact checks, not formal verification or runtime proof'}, indent=2))