Research source · python
verify_distance_two_normal_form.py
site/public/research-artifacts/distance-two-normal-form/verify_distance_two_normal_form.py
360 lines. Source is displayed for inspection; it is not executed by this page.
File fingerprint
SHA-256: cfdec1b8631c20afda846c8dc0788ebd38ae7d1efcf2e69c43ac6ba3dc6b532c
#!/usr/bin/env python3
"""Finite audit for FPRD-T160 distance-two shortcut normalization."""
from __future__ import annotations
import importlib.util
import itertools
import json
from dataclasses import dataclass
from pathlib import Path
MISSING = -1
SELF = -2
Descriptor = int | tuple[int, ...]
@dataclass(frozen=True)
class Scaffold:
labels: tuple[int, ...]
edges: tuple[tuple[int, ...], ...]
@property
def top(self) -> int:
return len(self.labels) - 1
def words(degree: int, distance: int, include_empty: bool = True) -> tuple[tuple[int, ...], ...]:
start = 0 if include_empty else 1
return tuple(
word
for length in range(start, distance + 1)
for word in itertools.product(range(degree), repeat=length)
)
def follow(scaffold: Scaffold, start: int, path: tuple[int, ...]) -> int:
if start == MISSING:
return MISSING
node = start
for port in path:
if node == MISSING:
return MISSING
node = scaffold.edges[node][port]
return node
def view(scaffold: Scaffold, node: int, radius: int):
if node == MISSING:
return ("missing",)
if radius == 0:
return ("label", scaffold.labels[node])
return (
"node",
scaffold.labels[node],
tuple(view(scaffold, target, radius - 1) for target in scaffold.edges[node]),
)
def root_view(scaffold: Scaffold, radius: int):
return ("missing",) if not scaffold.labels else view(scaffold, scaffold.top, radius)
def resolve_descriptor(scaffold: Scaffold, descriptor: Descriptor, new_index: int) -> int:
if descriptor == MISSING:
return MISSING
if descriptor == SELF:
return new_index
old_root = MISSING if not scaffold.labels else scaffold.top
return follow(scaffold, old_root, descriptor)
def extend(scaffold: Scaffold, label: int, descriptors: tuple[Descriptor, ...]) -> Scaffold:
new_index = len(scaffold.labels)
targets = tuple(resolve_descriptor(scaffold, descriptor, new_index) for descriptor in descriptors)
return Scaffold(scaffold.labels + (label,), scaffold.edges + (targets,))
def score(item) -> int:
if isinstance(item, int):
return item + 23
if isinstance(item, str):
return sum(ord(char) for char in item)
return 29 + sum((index + 7) * score(value) for index, value in enumerate(item))
@dataclass(frozen=True)
class OriginalMachine:
seed: int
degree: int
distance: int
labels: int = 3
controls: int = 4
def transition(self, state: int, symbol: int, old_view):
code = score((self.seed, state, symbol, old_view))
options: tuple[Descriptor, ...] = (MISSING, SELF, *words(self.degree, self.distance))
next_state = (state + symbol + code + self.seed) % self.controls
label = (code // 5 + state + symbol) % self.labels
descriptors = tuple(
options[(code + 11 * port + self.seed) % len(options)]
for port in range(self.degree)
)
return next_state, label, descriptors
def accepting(self, state: int) -> bool:
return state == self.seed % self.controls
@dataclass(frozen=True)
class ShortcutLayout:
original_degree: int
original_distance: int
port_words: tuple[tuple[int, ...], ...]
port_of: dict[tuple[int, ...], int]
@classmethod
def make(cls, degree: int, distance: int):
port_words = words(degree, distance, include_empty=False)
return cls(degree, distance, port_words, {word: index for index, word in enumerate(port_words)})
@property
def degree(self) -> int:
return len(self.port_words)
def shortcut_closure(original: Scaffold, layout: ShortcutLayout) -> Scaffold:
edges = []
for node in range(len(original.labels)):
edges.append(tuple(follow(original, node, word) for word in layout.port_words))
return Scaffold(original.labels, tuple(edges))
def reconstruct_original_view(shortcut: Scaffold, layout: ShortcutLayout):
if not shortcut.labels:
return ("missing",)
root = shortcut.top
def build(prefix: tuple[int, ...], remaining: int):
node = root if not prefix else shortcut.edges[root][layout.port_of[prefix]]
if node == MISSING:
return ("missing",)
if remaining == 0:
return ("label", shortcut.labels[node])
return (
"node",
shortcut.labels[node],
tuple(build(prefix + (port,), remaining - 1) for port in range(layout.original_degree)),
)
return build((), layout.original_distance)
def compile_shortcut_descriptor(
word: tuple[int, ...],
direct_descriptors: tuple[Descriptor, ...],
layout: ShortcutLayout,
) -> Descriptor:
remaining = word
while remaining:
direct = direct_descriptors[remaining[0]]
remaining = remaining[1:]
if direct == MISSING:
return MISSING
if direct == SELF:
continue
old_path = direct
suffix = remaining
if not old_path and not suffix:
return ()
if not old_path:
return (layout.port_of[suffix],)
if not suffix:
return (layout.port_of[old_path],)
return (layout.port_of[old_path], layout.port_of[suffix])
return SELF
def original_step(machine: OriginalMachine, state: int, scaffold: Scaffold, symbol: int):
next_state, label, descriptors = machine.transition(
state, symbol, root_view(scaffold, machine.distance)
)
return next_state, extend(scaffold, label, descriptors), descriptors
def compiled_step(
machine: OriginalMachine,
layout: ShortcutLayout,
state: int,
scaffold: Scaffold,
symbol: int,
):
old_view = reconstruct_original_view(scaffold, layout)
next_state, label, direct_descriptors = machine.transition(state, symbol, old_view)
shortcut_descriptors = tuple(
compile_shortcut_descriptor(word, direct_descriptors, layout)
for word in layout.port_words
)
assert all(
descriptor in (MISSING, SELF) or len(descriptor) <= 2
for descriptor in shortcut_descriptors
)
return next_state, extend(scaffold, label, shortcut_descriptors), shortcut_descriptors
def audit_machine_compilation() -> dict[str, int]:
machines = [
OriginalMachine(seed + 17 * distance + 31 * degree, degree, distance)
for degree in (1, 2)
for distance in (2, 3, 4)
for seed in range(2)
]
prefixes = [
word
for length in range(9)
for word in itertools.product((0, 1), repeat=length)
]
compiled_runs = 0
reconstructed_view_checks = 0
shortcut_edge_checks = 0
acceptance_checks = 0
distance_two_descriptor_checks = 0
for machine in machines:
layout = ShortcutLayout.make(machine.degree, machine.distance)
expected_degree = sum(machine.degree**length for length in range(1, machine.distance + 1))
assert layout.degree == expected_degree
for prefix in prefixes:
original = Scaffold((), ())
compiled = Scaffold((), ())
original_state = compiled_state = 0
for symbol in prefix:
assert reconstruct_original_view(compiled, layout) == root_view(
original, machine.distance
)
reconstructed_view_checks += 1
original_state, original, _ = original_step(
machine, original_state, original, symbol
)
compiled_state, compiled, descriptors = compiled_step(
machine, layout, compiled_state, compiled, symbol
)
assert compiled_state == original_state
expected = shortcut_closure(original, layout)
assert compiled == expected
shortcut_edge_checks += len(layout.port_words)
distance_two_descriptor_checks += len(descriptors)
assert machine.accepting(compiled_state) == machine.accepting(original_state)
acceptance_checks += 1
compiled_runs += 1
return {
"tiny_original_machines": len(machines),
"compiled_runs": compiled_runs,
"reconstructed_view_checks": reconstructed_view_checks,
"shortcut_edge_checks": shortcut_edge_checks,
"acceptance_checks": acceptance_checks,
"distance_two_descriptor_checks": distance_two_descriptor_checks,
}
def scaffold_family(node_count: int, degree: int):
labels = itertools.product(range(2), repeat=node_count)
edge_options = [
list(itertools.product([MISSING, *range(node + 1)], repeat=degree))
for node in range(node_count)
]
for label_row in labels:
for edges in itertools.product(*edge_options):
yield Scaffold(tuple(label_row), tuple(edges))
def audit_symbolic_installation() -> dict[str, int]:
cases = ((1, 4, 4), (2, 3, 3))
direct_descriptor_families = 0
symbolic_shortcuts = 0
old_scaffolds = 0
endpoint_matches = 0
self_shortcuts = 0
missing_shortcuts = 0
two_hop_shortcuts = 0
for degree, distance, nodes in cases:
layout = ShortcutLayout.make(degree, distance)
descriptor_options: tuple[Descriptor, ...] = (
MISSING,
SELF,
*words(degree, distance),
)
material = list(scaffold_family(nodes, degree))
old_scaffolds += len(material)
for direct in itertools.product(descriptor_options, repeat=degree):
direct_descriptor_families += 1
compiled_descriptors = tuple(
compile_shortcut_descriptor(word, direct, layout)
for word in layout.port_words
)
symbolic_shortcuts += len(compiled_descriptors)
self_shortcuts += sum(descriptor == SELF for descriptor in compiled_descriptors)
missing_shortcuts += sum(descriptor == MISSING for descriptor in compiled_descriptors)
two_hop_shortcuts += sum(
isinstance(descriptor, tuple) and len(descriptor) == 2
for descriptor in compiled_descriptors
)
for old in material:
original_new = extend(old, 1, direct)
compiled_old = shortcut_closure(old, layout)
compiled_new = extend(compiled_old, 1, compiled_descriptors)
expected = shortcut_closure(original_new, layout)
assert compiled_new.edges[-1] == expected.edges[-1]
endpoint_matches += len(layout.port_words)
return {
"symbolic_direct_descriptor_families": direct_descriptor_families,
"symbolic_shortcuts": symbolic_shortcuts,
"symbolic_old_scaffolds": old_scaffolds,
"symbolic_endpoint_matches": endpoint_matches,
"self_shortcuts": self_shortcuts,
"missing_shortcuts": missing_shortcuts,
"two_hop_shortcuts": two_hop_shortcuts,
}
def audit_strict_base_tier() -> dict[str, int]:
selector_path = Path(__file__).parents[1] / "replay-fanout" / "verify_persistent_selector.py"
spec = importlib.util.spec_from_file_location("persistent_selector", selector_path)
assert spec is not None and spec.loader is not None
module = importlib.util.module_from_spec(spec)
spec.loader.exec_module(module)
result = module.main()
assert result["ok"] is True
assert result["distance"] == 2
assert result["counts"]["residual_profiles"] == 2046
return {
"strictness_selector_words": result["counts"]["all_words"],
"strictness_residual_profiles": result["counts"]["residual_profiles"],
"strictness_selector_distance": result["distance"],
}
def main() -> None:
result: dict[str, object] = {
"scope": {
"machine_compilation": "12 machines, degree 1..2, original distance 2..4, all binary prefixes through length 8",
"symbolic_installation": "all direct descriptor rows for (degree,distance,nodes)=(1,4,4) and (2,3,3)",
"strictness": "persistent selector through total word length 10",
},
**audit_machine_compilation(),
**audit_symbolic_installation(),
**audit_strict_base_tier(),
"status": "pass",
}
output = Path(__file__).with_name("checker-output.json")
output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")
print(json.dumps(result, indent=2))
if __name__ == "__main__":
main()