check_late_prefix_cache.py

#!/usr/bin/env python3
"""Finite contract audit, not a native implementation or a hash simulation.

Exact tuple keys remove probabilistic collisions. We model FK section 6.2.1's
cached answers, including explicit full-key installation. Violating its
no-new-ancestor promise can leave an old sampled answer stale.
"""
from itertools import product
import json


def samples(word):
    n = len(word)
    return [word[:n >> b << b] for b in range(n.bit_length() - 1, -1, -1)
            if n & (1 << b)]


def longest(words, query):
    candidates = [w for w in words if query[:len(w)] == w]
    return max(candidates, key=len, default=None)


def install(words, cache, word):
    # Copying models retention only; Python cost is not a claimed native bound.
    out = dict(cache)
    for prefix in samples(word):
        if prefix not in out:
            out[prefix] = longest(words, prefix)
    out[word] = word
    return words | {word}, out


def cached(cache, query):
    sample = longest(cache, query)
    return cache[sample] if sample is not None else None


def main():
    universe = [tuple(w) for n in range(1, 5) for w in product((0, 1), repeat=n)]
    legal, illegal, stale, retained = 0, 0, 0, 0
    for first in universe:
        old_words, old = install(set(), {}, first)
        for second in universe:
            if first == second:
                continue
            words, new = install(old_words, old, second)
            allowed = first[:len(second)] != second
            for query in universe:
                assert cached(old, query) == longest(old_words, query)
                retained += 1
                agrees = cached(new, query) == longest(words, query)
                if allowed:
                    assert agrees
                    legal += 1
                else:
                    illegal += 1
                    stale += not agrees
    one = (1,) * 13
    words, old = install(set(), {}, one)
    words, new = install(words, old, (1,) * 4)
    query = (1,) * 8
    assert cached(old, query) is None
    assert cached(new, query) is None
    assert longest(words, query) == (1,) * 4
    # Generalized exact-key witness: many old length-8 samples below prefix 1.
    old_words, old = set(), {}
    for tail in product((0, 1), repeat=7):
        old_words, old = install(old_words, old, (1,) + tail + (0,) * 5)
    words, new = install(old_words, old, (1,))
    affected = 0
    for tail in product((0, 1), repeat=7):
        q = (1,) + tail
        assert cached(new, q) is None and longest(words, q) == (1,)
        affected += 1
    # Most recent or most specific contributor is not Boolean union.
    collision_checks = 0
    failures = {"newest_short": 0, "most_specific_long": 0}
    for short, long in product((False, True), repeat=2):
        union = short or long
        failures["newest_short"] += short != union
        failures["most_specific_long"] += long != union
        collision_checks += 1
    assert failures == {"newest_short": 1, "most_specific_long": 1}
    print(json.dumps(dict(status='passed', legal_query_checks=legal,
        forbidden_query_checks=illegal, stale_answers=stale,
        retained_version_checks=retained, explicit_unary_witness=True,
        stale_samples_in_branch_witness=affected,
        selected_collision_checks=collision_checks,
        scope='Exact-key cache contract only; no native complexity claim'),
        sort_keys=True))


if __name__ == '__main__':
    main()