"""Fast Lane FL-D4 composition proof over every declared application.

This is deliberately distinct from the generated-product runtime matrix. It
proves that every declared app closes over frozen job packs, App Blocks,
dependencies, and Starter IDs without inventing a semantic primitive. The
18-cell generated-product harness remains the stronger runtime proof.
"""

from __future__ import annotations

from dataclasses import dataclass

from src.domain.app_blocks.catalogs import default_known_packs, default_primitives
from src.domain.app_blocks.job_packs import JOB_FEATURE_PACKS
from src.domain.app_blocks.presentation_coverage import load_presentation_coverage
from src.domain.app_blocks.registry import load_default_registry
from src.domain.app_blocks.resolver import resolve_block
from src.domain.starter_library.archetypes import known_archetype_ids


@dataclass(frozen=True)
class FastLaneApplicationProof:
    application_id: str
    starter: str
    packs: tuple[str, ...]
    app_blocks: tuple[str, ...]
    composition_proven: bool
    findings: tuple[str, ...] = ()


def prove_declared_applications() -> list[FastLaneApplicationProof]:
    report = load_presentation_coverage()
    registry = load_default_registry()
    known_starters = known_archetype_ids()
    proofs: list[FastLaneApplicationProof] = []
    for app in report.declared_applications:
        findings: list[str] = []
        if app.starter not in known_starters:
            findings.append(f"unknown_starter:{app.starter}")
        blocks: set[str] = set()
        for pack_id in app.packs:
            pack = JOB_FEATURE_PACKS.get(pack_id)
            if pack is None:
                findings.append(f"unknown_pack:{pack_id}")
                continue
            blocks.update(pack.required_app_blocks)
        queue = list(blocks)
        visited: set[str] = set()
        while queue:
            block_id = queue.pop(0)
            if block_id in visited:
                continue
            visited.add(block_id)
            manifest = registry.get(block_id)
            if manifest is None or not manifest.implemented:
                findings.append(f"unimplemented_block:{block_id}")
                continue
            _packs, _primitives, nested, gaps, _configs, _optional = resolve_block(
                manifest,
                registry,
                primitives=default_primitives(),
                known_packs=default_known_packs(),
            )
            for gap in gaps:
                if gap.severity == "build_blocking":
                    findings.append(f"blocking_gap:{block_id}:{gap.id}")
            for nested_id in nested:
                if nested_id not in visited:
                    queue.append(nested_id)
                    blocks.add(nested_id)
        forbidden = set(app.forbidden_implicit)
        accidental = sorted(forbidden & blocks)
        if accidental:
            findings.append("forbidden_blocks:" + ",".join(accidental))
        proofs.append(FastLaneApplicationProof(
            application_id=app.id,
            starter=app.starter,
            packs=tuple(app.packs),
            app_blocks=tuple(sorted(blocks)),
            composition_proven=not findings,
            findings=tuple(findings),
        ))
    return proofs


def assert_declared_applications_composable() -> list[FastLaneApplicationProof]:
    proofs = prove_declared_applications()
    failures = [item for item in proofs if not item.composition_proven]
    if failures:
        details = "; ".join(f"{item.application_id}: {item.findings}" for item in failures)
        raise AssertionError(f"Fast Lane composition proof failed: {details}")
    return proofs