Research source · python
check_learned_filler_reuse.py
tools/research/check_learned_filler_reuse.py
249 lines. Source is displayed for inspection; it is not executed by this page.
File fingerprint
SHA-256: 608d5a384d1a72c8d3b69a3838204fff2d19960a02d04829274358536305fce6
#!/usr/bin/env python3
"""Finite audit of learned fillers with a fixed occupied-store fibre bound.
Independent direct-owner activation versus immutable normalized bit masks.
Python dictionaries/copies are oracle machinery, not a native implementation.
The service audit counts abstract jobs; it is not a native timing measurement.
Run without arguments for deterministic exhaustive and seeded checks.
"""
from itertools import product, permutations
import json
import random
def words(n):
return [''.join(w) for w in product('01', repeat=n)]
def encode(v):
return ''.join('0' + b for b in v)
def split(beta):
"""Pair parser independent of any namespace's learned key length."""
v = ''
for p in range(0, len(beta) - 1, 2):
pair = beta[p:p + 2]
if pair == '11':
if not v:
raise ValueError('empty key')
return v, beta[p + 2:]
if pair[0] != '0':
raise ValueError('invalid pair')
v += pair[1]
raise ValueError('missing delimiter')
def key(b, n):
assert len(b) == 2 * n + 1 and b[0] == '1'
v, _ = split(b[n + 1:])
return b[1:n + 1] + encode(v) + '11'
class Registry:
def __init__(self, n, capacity):
self.n, self.capacity = n, capacity
self.full, self.count = {}, {}
def add(self, b):
# Exact spelling lookup occurs before normalized-key count changes.
k = key(b, self.n)
if b in self.full:
return self.full[b]
slot = self.count.get(k, 0)
if slot == self.capacity:
raise ValueError('fibre overflow')
self.full[b] = slot
self.count[k] = slot + 1
return slot
def update(state, b, alias, registry):
if b not in registry.full:
raise ValueError('unknown owner')
if alias not in (0, 1):
raise ValueError('invalid alias')
literal, normalized = state
if alias:
return state
next_literal, next_normalized = set(literal), dict(normalized)
next_literal.add(b)
k, slot = key(b, registry.n), registry.full[b]
next_normalized[k] = next_normalized.get(k, 0) | (1 << slot)
return frozenset(next_literal), next_normalized
def mapped(program, t):
return ''.join(program[t[:j]] for j in range(1, len(t) + 1))
def owner(view, z, n):
alpha, ell, filler, program = view
if len(z) != n:
return None
if z[:n - ell] == '0' * (n - ell):
t = z[n - ell:]
return '1' + alpha + encode(mapped(program, t)) + '11' + filler
return '1' + alpha + z
def query(state, view, z, support, registry):
# The actual support lane is finite data; no reconstructed owner lookup.
if z not in support:
return False
alpha, ell, _, program = view
literal, normalized = state
if z[:registry.n - ell] == '0' * (registry.n - ell):
t = z[registry.n - ell:]
k = alpha + encode(mapped(program, t)) + '11'
return bool(normalized.get(k, 0) & (1 << support[z]))
return '1' + alpha + z in literal
def schedule(n, ell):
# One FIFO: initial alpha/setup jobs; two jobs per late transformed bit;
# the last bit additionally releases the two delimiter jobs.
pending = n + 2
trace = []
for p in range(1, n + 1):
released = (2 if p > n - ell else 0) + (2 if p == n else 0)
pending += released
done = min(4, pending)
pending -= done
trace.append((released, done, pending))
return pending, trace
def main():
counts = dict(parser=0, registry=0, reads=0, snapshots=0, schedules=0,
rejected=0, counterexamples=0)
for length in range(10):
for beta in words(length):
# Independent language-membership oracle enumerates decompositions.
candidates = [(v, beta[2 * k + 2:])
for k in range(1, (length - 2) // 2 + 1)
for v in words(k)
if beta.startswith(encode(v) + '11')]
try:
result = split(beta)
assert candidates == [result]
except ValueError:
assert not candidates
counts['parser'] += 1
n = 8
alpha = '0' * n
owners = ['1' + alpha + encode('1') + '11' + w for w in words(4)[:3]]
for order in permutations(owners):
for capacity in (1, 2, 3):
r = Registry(n, capacity)
for j, b in enumerate(order):
before = (dict(r.full), dict(r.count))
if j >= capacity:
try:
r.add(b)
raise AssertionError('accepted overflow')
except ValueError:
assert (r.full, r.count) == before
counts['rejected'] += 1
continue
assert r.add(b) == j
frozen = (dict(r.full), dict(r.count))
assert r.add(b) == j
assert (r.full, r.count) == frozen
counts['registry'] += 2
# Exhaustive activation and alias combinations within this fibre.
stored = list(r.full)
for statuses in product((0, 1), repeat=len(stored)):
s = (frozenset(), {})
history = [(s, frozenset())]
direct = set()
for b, alias in zip(stored, statuses):
s = update(s, b, alias, r)
if alias == 0:
direct.add(b)
history.append((s, frozenset(direct)))
for old, expected in history:
for b in stored:
actual = bool(old[1].get(key(b, n), 0) & (1 << r.full[b]))
assert actual == (b in expected)
counts['reads'] += 1
counts['snapshots'] += 1
rng = random.Random(241)
for trial in range(24):
n, capacity = 20, 3
registry = Registry(n, capacity)
views, supports = [], []
# Multiple lengths and arbitrary independent fillers at shared keys.
for ell in (1, 2, 3, 4):
program = {p: rng.choice('01') for j in range(1, ell + 1) for p in words(j)}
# Every view has an actual identity-key seed at t = 0^ell.
for j in range(1, ell + 1):
program['0' * j] = '0'
alpha = format(ell, '020b')
fillers = set()
while len(fillers) < capacity:
fillers.add(''.join(rng.choice('01') for _ in range(n - 2 * ell - 2)))
for filler in sorted(fillers):
view = (alpha, ell, filler, program)
support = {}
for t in words(ell):
z = '0' * (n - ell) + t
b = owner(view, z, n)
slot = registry.add(b)
if rng.randrange(4) or t == '0' * ell:
support[z] = slot
# Actual ordinary identity rows use the same known owner.
support[b[n + 1:]] = slot
views.append(view)
supports.append(support)
names = list(registry.full)
states = {'s0': (frozenset(), {}), 's1': (frozenset(), {})}
direct = {'s0': set(), 's1': set()}
history = []
for step in range(80):
source, b, alias = rng.choice(tuple(states)), rng.choice(names), rng.randrange(2)
states[source] = update(states[source], b, alias, registry)
if alias == 0:
direct[source].add(b)
history.append((dict(states), {s: frozenset(v) for s, v in direct.items()}))
for states_then, direct_then in history[::5]:
for source in states_then:
for view, support in zip(views, supports):
candidates = set(support)
ell = view[1]
candidates.update('0' * (n - ell) + t for t in words(ell))
candidates.update(('0', '1' * (n + 1), '1' * n))
for z in candidates:
expected = z in support and owner(view, z, n) in direct_then[source]
assert query(states_then[source], view, z, support, registry) == expected
counts['reads'] += 1
counts['snapshots'] += 1
try:
update(states['s0'], 'unknown', 0, registry)
raise AssertionError('accepted unknown owner')
except ValueError:
counts['rejected'] += 1
for ell in range(1, 65):
for n in range(4 * ell + 4, 4 * ell + 37):
pending, trace = schedule(n, ell)
assert pending == 0 and trace[-1][0] == 4
assert trace[n - ell - 1][2] == 0
counts['schedules'] += 1
# Removing the finite slot produces a false positive across two fillers.
r = Registry(8, 2)
for b in owners[:2]:
r.add(b)
state = update((frozenset(), {}), owners[0], 0, r)
assert key(owners[0], 8) == key(owners[1], 8)
assert state[1][key(owners[1], 8)] != 0
assert not state[1][key(owners[1], 8)] & (1 << r.full[owners[1]])
counts['counterexamples'] += 1
print(json.dumps({'status': 'pass', 'seed': 241, 'checks': counts}, sort_keys=True))
if __name__ == '__main__':
main()