verify_local_block_tabulation.py

"""Finite algorithmic checks for the written local block-table construction.

The Store records immutable bounded-arity nodes and charges each access/allocation.
Counts measure heap accesses/allocations, not control, input or root-copy steps.
Python is the execution harness, not a formally certified finite-state compiler.
The paper supplies uniformity, root bounds and unrestricted asymptotic proofs.
"""
import json
import random
from pathlib import Path

class Store:
    def __init__(self):
        self.nodes = [('End', ())]
        self.steps = 0
    def new(self, tag, *fields):
        assert len(fields) <= 3
        assert all(isinstance(p, int) and 0 <= p < len(self.nodes) for p in fields)
        self.steps += 1
        self.nodes.append((tag, tuple(fields)))
        return len(self.nodes)-1
    def tag(self, p):
        self.steps += 1
        return self.nodes[p][0]
    def field(self, p, i):
        self.steps += 1
        return self.nodes[p][1][i]

def reverse(s, p, bit=False):
    q = 0
    while s.tag(p) != 'End':
        if bit:
            q = s.new(s.tag(p), q)
            p = s.field(p, 0)
        else:
            q = s.new('List', s.field(p, 0), q)
            p = s.field(p, 1)
    return q

def input_bits(s, bits):
    # Host supplies successive symbols. Reversal restores serial order.
    q = 0
    for b in bits:
        q = s.new('One' if b else 'Zero', q)
    return reverse(s, q, True)

def ruler(s, k):
    q = 0
    for _ in range(k):  # unary header symbols from the host
        q = s.new('Tick', q)
    return q

def zeros(s, ticks):
    q = 0
    while s.tag(ticks) != 'End':
        q = s.new('Zero', q)
        ticks = s.field(ticks, 0)
    return q

def chunks(s, bits, K):
    out = 0
    while s.tag(bits) != 'End':
        t, rev = K, 0
        while s.tag(t) != 'End':
            label = s.tag(bits)
            if label == 'End':
                label = 'Zero'
            else:
                bits = s.field(bits, 0)
            rev = s.new(label, rev)
            t = s.field(t, 0)
        out = s.new('List', reverse(s, rev, True), out)
    return reverse(s, out)

def leaf_value(s, block, prefix, K):
    assignment = reverse(s, prefix, True)
    u, v, t = assignment, assignment, K
    while s.tag(t) != 'End':
        v = s.field(v, 0)
        t = s.field(t, 0)
    parity = 0
    rows = block
    while s.tag(rows) != 'End':
        ub = s.tag(u) == 'One'
        row, vc = s.field(rows, 0), v
        while s.tag(row) != 'End':
            parity ^= ub and s.tag(row) == 'One' and s.tag(vc) == 'One'
            row, vc = s.field(row, 0), s.field(vc, 0)
        rows, u = s.field(rows, 1), s.field(u, 0)
    return s.new('Leaf1' if parity else 'Leaf0')

def build_trie(s, block, K):
    # Two copies of unary ruler; no integer depth or recursive Python stack.
    D, t = K, K
    while s.tag(t) != 'End':
        D = s.new('Tick', D)
        t = s.field(t, 0)
    depth, prefix, stack, result = D, 0, 0, 0
    descend = True
    while True:
        if descend:
            if s.tag(depth) != 'End':
                rest = s.field(depth, 0)
                stack = s.new('Left', rest, prefix, stack)
                prefix = s.new('Zero', prefix)
                depth = rest
                continue
            result = leaf_value(s, block, prefix, K)
            descend = False
        label = s.tag(stack)
        if label == 'End':
            return result
        if label == 'Left':
            depth = s.field(stack, 0)
            prefix = s.new('One', s.field(stack, 1))
            parent = s.field(stack, 2)
            stack = s.new('Right', result, parent)
            descend = True
        else:
            result = s.new('Branch', s.field(stack, 0), result)
            stack = s.field(stack, 1)

def prepare_matrix(s, serial_bits, N, K):
    # Flat row-major input: unary width cursor, no supplied row boundaries.
    rev, row_rev, column, row_count = 0, 0, N, N
    for bit in serial_bits:  # host delivers the next input bit
        row_rev = s.new('One' if bit else 'Zero', row_rev)
        column = s.field(column, 0)
        if s.tag(column) == 'End':
            row = reverse(s, row_rev, True)
            rev = s.new('List', chunks(s, row, K), rev)
            row_rev, column = 0, N
            row_count = s.field(row_count, 0)
    assert s.tag(row_count) == 'End' and s.tag(row_rev) == 'End'
    rows = reverse(s, rev)
    z = zeros(s, K)
    template, zr = s.field(rows, 0), 0
    while s.tag(template) != 'End':
        zr = s.new('List', z, zr)
        template = s.field(template, 1)
    zero_row = reverse(s, zr)
    out = 0
    while s.tag(rows) != 'End':
        t, br = K, 0
        while s.tag(t) != 'End':
            if s.tag(rows) == 'End':
                rc = zero_row
            else:
                rc, rows = s.field(rows, 0), s.field(rows, 1)
            br = s.new('List', rc, br)
            t = s.field(t, 0)
        band, table_row = reverse(s, br), 0
        while s.tag(s.field(band, 0)) != 'End':
            scan, block_rev, next_rev = band, 0, 0
            while s.tag(scan) != 'End':
                rc = s.field(scan, 0)
                block_rev = s.new('List', s.field(rc, 0), block_rev)
                next_rev = s.new('List', s.field(rc, 1), next_rev)
                scan = s.field(scan, 1)
            block = reverse(s, block_rev)
            root = build_trie(s, block, K)
            table_row = s.new('List', root, table_row)
            band = reverse(s, next_rev)
        out = s.new('List', reverse(s, table_row), out)
    return reverse(s, out)

def prepare_query(s, u, v, K):
    return chunks(s, input_bits(s, u), K), chunks(s, input_bits(s, v), K)

def query(s, matrix, ublocks, vblocks):
    parity = 0
    while s.tag(matrix) != 'End':
        blockrow = s.field(matrix, 0)
        u = s.field(ublocks, 0)
        vc = vblocks
        while s.tag(blockrow) != 'End':
            trie = s.field(blockrow, 0)
            cur = u
            while s.tag(cur) != 'End':
                trie = s.field(trie, 1 if s.tag(cur) == 'One' else 0)
                cur = s.field(cur, 0)
            cur = s.field(vc, 0)
            while s.tag(cur) != 'End':
                trie = s.field(trie, 1 if s.tag(cur) == 'One' else 0)
                cur = s.field(cur, 0)
            label = s.tag(trie)
            assert label in ('Leaf0', 'Leaf1')
            parity ^= label == 'Leaf1'
            blockrow, vc = s.field(blockrow, 1), s.field(vc, 1)
        matrix, ublocks = s.field(matrix, 1), s.field(ublocks, 1)
    return int(parity)

def oracle(A, u, v):
    return sum(u[i]*A[i][j]*v[j] for i in range(len(u)) for j in range(len(v))) % 2

def run():
    results=[]
    rng=random.Random(20261003)
    for n in range(1,8):
        for k in range(1,min(n,3)+1):
            matrices = ([[((a >> (i*n+j))&1) for j in range(n)] for i in range(n)] for a in range(1 << (n*n))) if n<=2 else ([[rng.randrange(2) for _ in range(n)] for _ in range(n)] for _ in range(4))
            cases=0;max_p=max_nodes=max_q=max_qprep=0
            for A in matrices:
                s=Store();K=ruler(s,k);N=ruler(s,n);root=prepare_matrix(s,(b for row in A for b in row),N,K)
                matrix_nodes=tuple(s.nodes);psteps=s.steps
                max_p=max(max_p,psteps);max_nodes=max(max_nodes,len(s.nodes))
                pairs=((u,v) for u in range(1<<n) for v in range(1<<n)) if n<=2 else ((rng.randrange(1<<n),rng.randrange(1<<n)) for _ in range(24))
                for ui,vi in pairs:
                    u=[(ui>>i)&1 for i in range(n)];v=[(vi>>i)&1 for i in range(n)]
                    prep_start=s.steps
                    query_base=len(s.nodes)
                    query_K=ruler(s,k)  # independently loaded public header
                    qu,qv=prepare_query(s,u,v,query_K)
                    assert all(p == 0 or p >= query_base for _, fs in s.nodes[query_base:] for p in fs)
                    max_qprep=max(max_qprep,s.steps-prep_start)
                    before=s.steps;nodes=len(s.nodes)
                    assert query(s,root,qu,qv)==oracle(A,u,v)
                    assert len(s.nodes)==nodes
                    assert tuple(s.nodes[:len(matrix_nodes)])==matrix_nodes
                    max_q=max(max_q,s.steps-before);cases+=1
                m=(n+k-1)//k
                assert max_q <= 40*m*m*(k+1)+20*m+20
            results.append(dict(n=n,k=k,padded=(n+k-1)//k*k,cases=cases,max_matrix_heap_operations=max_p,max_matrix_nodes=max_nodes,max_query_heap_operations=max_q,max_query_preparation_heap_operations=max_qprep))
    return {'status':'passed','scope':'all matrices/queries for n<=2; four seeded matrices and 24 query pairs each for n=3..7, all k<=min(n,3); host Python witness, no formal compiler verification','results':results}

if __name__ == '__main__':
    print(json.dumps(run(),indent=2))