#!/usr/bin/env python3
"""Finite checks for Run 08's completed simultaneous-record interface.

This checks boundary witnesses and current statement markers.  The general
factorization and compiler-completion arguments are proved in run-08.md.
"""

from collections import defaultdict
from dataclasses import dataclass
from itertools import product
import json
from pathlib import Path


MISSING = -1


@dataclass(frozen=True)
class Graph:
    labels: tuple
    edges: tuple
    root: int


def native_view(graph, node, radius):
    if node == MISSING:
        return None
    if radius == 0:
        return graph.labels[node]
    return (
        graph.labels[node],
        tuple(native_view(graph, child, radius - 1) for child in graph.edges[node]),
    )


def alias_at_root(graph):
    left, right = graph.edges[graph.root]
    return left != MISSING and left == right


def follow(graph, node, word):
    for port in word:
        if node == MISSING:
            return MISSING
        node = graph.edges[node][port]
    return node


def explicit_alias_witness():
    # Node 0 is the unlabelled base. Nodes 1 and 2 are behaviorally identical
    # old leaves. Node 3 is the current root.
    labels = (None, "leaf", "leaf", "root")
    common = ((MISSING, MISSING), (MISSING, MISSING), (MISSING, MISSING))
    shared = Graph(labels, common + ((1, 1),), 3)
    split = Graph(labels, common + ((1, 2),), 3)

    assert alias_at_root(shared) and not alias_at_root(split)
    for radius in range(9):
        assert native_view(shared, shared.root, radius) == native_view(split, split.root, radius)

    # A fixed plan can copy both old addresses. Their compiled path endpoints
    # preserve the source aliasing even though the plan cannot branch on it.
    copied_shared = (follow(shared, shared.root, (0,)), follow(shared, shared.root, (1,)))
    copied_split = (follow(split, split.root, (0,)), follow(split, split.root, (1,)))
    assert copied_shared[0] == copied_shared[1]
    assert copied_split[0] != copied_split[1]
    return {
        "native_depths_checked": 9,
        "shared_alias_predicate": alias_at_root(shared),
        "split_alias_predicate": alias_at_root(split),
        "copied_alias_preserved": True,
    }


def finite_alias_buckets():
    # Vary the two root targets over missing, base, and two bisimilar leaves.
    labels = (None, "leaf", "leaf", "root")
    old = ((MISSING, MISSING), (MISSING, MISSING), (MISSING, MISSING))
    endpoints = (MISSING, 0, 1, 2)
    graphs = [Graph(labels, old + ((left, right),), 3)
              for left, right in product(endpoints, repeat=2)]
    result = {}
    for radius in range(6):
        buckets = defaultdict(set)
        for graph in graphs:
            buckets[repr(native_view(graph, graph.root, radius))].add(alias_at_root(graph))
        result[str(radius)] = {
            "view_buckets": len(buckets),
            "buckets_mixing_alias_and_nonalias": sum(len(values) > 1 for values in buckets.values()),
        }
    assert any(item["buckets_mixing_alias_and_nonalias"] > 0 for item in result.values())
    assert result["5"]["buckets_mixing_alias_and_nonalias"] > 0
    return result


def statement_markers():
    root = Path(__file__).resolve().parents[2]
    objects = root / "research-artifacts/scaffold-proof-review/history/objects"
    direct = (objects / "d34d79ed8bffa82a7e9c2ce726bba32d131c4ffbe9a93b90fb0fd3cd929fd6c3.txt").read_text()
    causal = (objects / "2b0910f423c0a56136a7d1c293c57ff5f6361ee40bf5d777aa4d1da7aaaae716.txt").read_text()
    initialization = json.loads((root / "research-artifacts/scaffold-proof-review/virtual-initialization-output.json").read_text())

    checks = {
        "direct_fixed_virtual_initial_graph": "fixed finite, immutable, pointer-closed initial record graph" in direct,
        "direct_positive_degree": "d=\\max\\{1,s+Aq\\}" in direct,
        "direct_identity_exclusion": "does not branch on pointer identity" in direct,
        "causal_identity_exclusion": "does not branch on physical pointer identity" in causal,
        "causal_unqualified_degree": "d=s+Aq" in causal,
        "causal_inductive_step_assumes_decoded_old_heap": "Assume the old physical heap decodes correctly" in causal,
        "causal_virtual_initial_clause_absent": "fixed finite, immutable, pointer-closed initial record graph" not in causal,
        "prior_virtual_initialization_audit_passed": initialization["status"] == "pass",
    }
    assert all(checks.values())
    return checks, initialization


checks, initialization = statement_markers()
result = {
    "status": "pass",
    "explicit_alias_witness": explicit_alias_witness(),
    "finite_alias_buckets": finite_alias_buckets(),
    "statement_markers": checks,
    "virtual_initialization_audit_reused": {
        "initial_graph_root_configurations": initialization["initial_graph_root_configurations"],
        "one_step_checks": initialization["one_step_checks"],
        "two_step_checks": initialization["two_step_checks"],
    },
    "proved_boundary": {
        "transition_choice_must_factor_through_native_view": True,
        "physical_alias_is_not_native_view_data": True,
        "a_fixed_plan_can_preserve_existing_aliases": True,
        "fixed_pointer_closed_initial_data_can_be_virtualized": True,
    },
    "scope": "Finite witnesses and source markers; the general theorem is proved in Run 08.",
}

print(json.dumps(result, indent=2, sort_keys=True))