verify_composition_access.py

#!/usr/bin/env python3
"""Finite corroboration only; the unrestricted argument is in the companion note."""
import hashlib
import itertools
import json
from pathlib import Path


def gate(x, z, lo, hi):
    return [(x, -z, lo), (x, z, -lo), (-x, -z, hi), (-x, z, -hi)]


def formula(b, mask):
    m = 1 << b
    z = lambda node: b + node  # complete binary heap numbering 1..2m-1
    clauses = []
    for node in range(1, m):
        x = node.bit_length()
        clauses.extend(gate(x, z(node), z(2 * node), z(2 * node + 1)))
    for a in range(m):
        clauses.append((z(m + a) if (mask >> a) & 1 else -z(m + a),))
    clauses.append((z(1),))
    return clauses


def holds(clauses, assignment):
    return all(any(assignment[abs(lit)] == (lit > 0) for lit in c) for c in clauses)


def project_bruteforce(b, mask, clauses):
    m = 1 << b
    relation = 0
    valuations = 0
    for a in range(m):
        boundary = {i + 1: bool((a >> (b - i - 1)) & 1) for i in range(b)}
        sat = False
        for bits in itertools.product((False, True), repeat=2 * m - 1):
            assignment = dict(boundary)
            assignment.update({b + j + 1: value for j, value in enumerate(bits)})
            sat |= holds(clauses, assignment)
            valuations += 1
        if sat:
            relation |= 1 << a
    return relation, valuations


class Heap:
    def __init__(self):
        self.nodes = [("End", 0)]
        self.old_probes = 0

    def cons(self, bit, tail):
        self.nodes.append(("One" if bit else "Zero", tail))
        return len(self.nodes) - 1

    def table(self, bits):
        p = 0
        for bit in reversed(bits):
            p = self.cons(bit, p)
        return p

    def observe(self, p, initial_size):
        if p < initial_size:
            self.old_probes += 1
        return self.nodes[p][0]

    def decoded(self, p):
        out = []
        while self.nodes[p][0] != "End":
            label, p = self.nodes[p]
            out.append(label == "One")
        return out

    def join(self, left, right):
        initial_size = len(self.nodes)
        acc = 0
        any_one = False
        positions = 0
        while True:
            a = self.observe(left, initial_size)
            b = self.observe(right, initial_size)
            if a == "End" or b == "End":
                assert a == b == "End"
                break
            bit = a == b == "One"
            any_one |= bit
            acc = self.cons(bit, acc)
            left = self.nodes[left][1]
            right = self.nodes[right][1]
            positions += 1
        out = 0
        while self.nodes[acc][0] != "End":
            bit, acc = self.nodes[acc]
            out = self.cons(bit == "One", out)
        assert len(self.nodes) - initial_size == 2 * positions
        return out, any_one


def main():
    gate_cases = 0
    for x, z, lo, hi in itertools.product((False, True), repeat=4):
        assert holds(gate(1, 2, 3, 4), {1: x, 2: z, 3: lo, 4: hi}) == (z == (hi if x else lo))
        gate_cases += 1
    projection_cases = valuations = 0
    for b in range(3):
        for mask in range(1 << (1 << b)):
            actual, n = project_bruteforce(b, mask, formula(b, mask))
            assert actual == mask
            projection_cases += 1
            valuations += n
    # Omitting the required root unit destroys the advertised relation.
    without_root, _ = project_bruteforce(1, 0, formula(1, 0)[:-1])
    assert without_root == 3
    size_rows = []
    for b in range(13):
        m = 1 << b
        cs = formula(b, 0)
        v, c, l = b + 2 * m - 1, len(cs), sum(map(len, cs))
        assert (c, l) == (5 * m - 3, 13 * m - 11)
        assert max(abs(x) for clause in cs for x in clause) == v
        k = v.bit_length()
        if b >= 1:
            assert k == b + 2
        size_rows.append(dict(b=b, m=m, variables=v, clauses=c, literals=l,
                              identifier_bits=k, body_bits=2*c + (k+1)*l))
    fooling_pairs = scan_pairs = 0
    for b in range(4):
        m = 1 << b
        universe = (1 << m) - 1
        for x in range(1 << m):
            assert not (x & (universe ^ x))
            for y in range(x):
                assert (x & (universe ^ y)) or (y & (universe ^ x))
                fooling_pairs += 1
            for y in range(1 << m):
                heap = Heap()
                left_bits = [bool((x >> i) & 1) for i in range(m)]
                right_bits = [bool((y >> i) & 1) for i in range(m)]
                left, right = heap.table(left_bits), heap.table(right_bits)
                before = tuple(heap.nodes)
                out, answer = heap.join(left, right)
                assert tuple(heap.nodes[:len(before)]) == before
                assert heap.decoded(left) == left_bits and heap.decoded(right) == right_bits
                assert heap.decoded(out) == [a and b for a, b in zip(left_bits, right_bits)]
                assert answer == bool(x & y)
                assert heap.old_probes == 2 * m + 2
                scan_pairs += 1
    source = Path(__file__)
    result = dict(status="passed", date="2026-10-01", gate_assignments=gate_cases,
                  complete_projection_widths=[0, 1, 2], projection_formulas=projection_cases,
                  complete_boolean_valuations=valuations, omitted_root_negative_control=True,
                  fooling_set_widths=[0, 1, 2, 3], distinct_fooling_pair_comparisons=fooling_pairs,
                  immutable_scan_widths=[0, 1, 2, 3], immutable_scan_pairs=scan_pairs,
                  size_rows=size_rows,
                  source_sha256=hashlib.sha256(source.read_bytes()).hexdigest(),
                  scope="Finite gate/projection/fooling-family/size and immutable-list model checks.",
                  not_verified=["unrestricted lower bound", "all opaque-pointer implementations",
                                "machine transfer", "Python execution cost", "Lean proof"])
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()