orchestrata_ultimate.factory.formalization.c4

Reference › orchestrata_ultimate › factory › formalization › c4

c4 holds the model-free logical detectors over a declared formalization (SPEC-033 row B26, requirement REQ-033-C4, ADR-0022). A Formalization has finite, small domains, so the module searches exhaustively: solutions yields every assignment over the variables that satisfies all constraints (_satisfies checks one constraint). MAX_ASSIGNMENTS (1,000,000) is an explicit ceiling; beyond it the module raises FormalizationTooLarge and never samples silently. check_contradiction returns a ContradictionFinding naming the conflicting constraint ids and sources when no assignment satisfies the set. check_under_constraint returns an UnderConstraintFinding with two witness assignments when the solutions differ on at least two projections of the observable variables. run_c4 runs both and returns a C4Report that includes the observable solution count. Following ADR-0026 each finding carries concrete witnesses, never a bare boolean. C4 speaks only about the declared formalization (ADR-0011): a constraint missing from the declaration is invisible to it. The dor_bridge, the decision phase and the scripts.factory_c4 CLI import it; tests are in tests/factory/test_c4_detectors.py.

At a glance

Class diagram

Dependency diagram

API

Classes

FormalizationTooLarge

Bases: Exception · Line 37

Raised when a formalization's cartesian product exceeds MAX_ASSIGNMENTS.

ContradictionFinding (dataclass)

Decorators: dataclass(frozen=True) · Line 122

The constraint set admits no solution -- a counterexample-free, plain contradiction.

UnderConstraintFinding (dataclass)

Decorators: dataclass(frozen=True) · Line 138

The constraint set admits >=2 materially different solutions.

C4Report (dataclass)

Decorators: dataclass(frozen=True) · Line 154

The combined C4 result for one requirement's declared formalization.

Functions

Source

Permalink: https://gitlab.com/MSamy/orchestrata-ultimate-architecture/-/blob/a4cbc2bdf/src/orchestrata_ultimate/factory/formalization/c4.py

"""Model-free logical detectors over a declared formalization (B26, REQ-033-C4).

Domains in a declared formalization are finite and small -- this formalizes
ACs, not physics -- so exhaustive search over the cartesian product of
variable domains, filtered by the constraint set, is CORRECT and sufficient;
this module caps nothing except an explicit, loud ceiling
(:data:`MAX_ASSIGNMENTS`) past which it refuses to silently sample and raises
:class:`FormalizationTooLarge` instead.

Per ADR-0026's counterexample-enumeration discipline, every finding here
carries specific witnesses (concrete assignments, or the actual conflicting
constraint ids/sources), never a bare boolean.

C4 speaks only about the DECLARED formalization (ADR-0011's boundary): a
missing constraint that was also missing from the declaration is invisible
to C4, and no return type here claims completeness of the underlying
requirement -- only of the constraint set as written.
"""

from __future__ import annotations

import dataclasses
import itertools
from collections.abc import Iterator
from dataclasses import dataclass

from orchestrata_ultimate.core.base.traces import traces
from orchestrata_ultimate.factory.formalization.models import (
    Constraint,
    ConstraintKind,
    Formalization,
)

MAX_ASSIGNMENTS = 1_000_000


class FormalizationTooLarge(Exception):
    """Raised when a formalization's cartesian product exceeds MAX_ASSIGNMENTS.

    An explicit, loud limit is honest; a silent sample is not (B26 brief).
    """


def _product_size(formalization: Formalization) -> int:
    size = 1
    for variable in formalization.variables:
        size *= len(variable.domain.values)
    return size


def _satisfies(assignment: dict[str, str], constraint: Constraint) -> bool:
    if constraint.kind is ConstraintKind.REQUIRE:
        tup = tuple(assignment[name] for name in constraint.vars)
        return tup in constraint.tuples
    if constraint.kind is ConstraintKind.FORBID:
        tup = tuple(assignment[name] for name in constraint.vars)
        return tup not in constraint.tuples
    # ConstraintKind.IMPLIES
    assert constraint.antecedent is not None
    assert constraint.consequent_var is not None
    antecedent_var, antecedent_value = constraint.antecedent
    if assignment[antecedent_var] != antecedent_value:
        return True
    return assignment[constraint.consequent_var] in constraint.consequent_values


def solutions(formalization: Formalization) -> Iterator[dict[str, str]]:
    """Yield every assignment over ``formalization.variables`` satisfying
    all constraints.

    Exhaustive cartesian-product search -- correct and sufficient for the
    small, finite domains a declared formalization is expected to have.

    Raises:
        FormalizationTooLarge: If the cartesian product of variable domains
            exceeds :data:`MAX_ASSIGNMENTS`.
    """
    size = _product_size(formalization)
    if size > MAX_ASSIGNMENTS:
        raise FormalizationTooLarge(
            f"formalization {formalization.requirement_id!r} has {size} possible "
            f"assignments (cartesian product of variable domains), exceeding "
            f"MAX_ASSIGNMENTS={MAX_ASSIGNMENTS}"
        )
    names = [v.name for v in formalization.variables]
    domains = [v.domain.values for v in formalization.variables]
    for combo in itertools.product(*domains):
        assignment = dict(zip(names, combo, strict=True))
        if all(_satisfies(assignment, c) for c in formalization.constraints):
            yield assignment


def _has_solution(formalization: Formalization) -> bool:
    for _ in solutions(formalization):
        return True
    return False


def _observable_names(formalization: Formalization) -> tuple[str, ...]:
    return tuple(v.name for v in formalization.variables if v.observable)


def _observable_projections(
    formalization: Formalization,
) -> dict[tuple[str, ...], dict[str, str]]:
    """Map each distinct observable projection to one witness assignment.

    Insertion order follows the deterministic cartesian-product enumeration
    order of :func:`solutions`, so the first two entries of the returned dict
    are a deterministic pair of distinct witnesses.
    """
    observable = _observable_names(formalization)
    seen: dict[tuple[str, ...], dict[str, str]] = {}
    for assignment in solutions(formalization):
        projection = tuple(assignment[name] for name in observable)
        if projection not in seen:
            seen[projection] = assignment
    return seen


@dataclass(frozen=True)
class ContradictionFinding:
    """The constraint set admits no solution -- a counterexample-free,
    plain contradiction.

    ``conflicting_constraint_ids``/``conflicting_sources`` are an
    approximate-minimal unsatisfiable core (see :func:`check_contradiction`),
    not guaranteed globally minimal, but always itself unsatisfiable and
    named down to the actual conflicting constraints/sentences.
    """

    requirement_id: str
    conflicting_constraint_ids: tuple[str, ...]
    conflicting_sources: tuple[str, ...]


@dataclass(frozen=True)
class UnderConstraintFinding:
    """The constraint set admits >=2 materially different solutions.

    ``witness_a``/``witness_b`` are two FULL concrete assignments (not just
    the observable projection) that differ on ``differing_observable_vars``
    -- the AC-observable variables where they diverge (ADR-0022's
    materiality criterion: only observable variables count).
    """

    requirement_id: str
    differing_observable_vars: tuple[str, ...]
    witness_a: dict[str, str]
    witness_b: dict[str, str]


@dataclass(frozen=True)
class C4Report:
    """The combined C4 result for one requirement's declared formalization.

    NO field here claims completeness of the requirement -- C4 speaks only
    about the DECLARED formalization; a missing constraint that was also
    missing from the declaration is invisible to C4 (ADR-0011's boundary).
    """

    requirement_id: str
    contradiction: ContradictionFinding | None
    under_constraint: UnderConstraintFinding | None
    solution_count_observable: int


@traces(spec="033", reqs=["REQ-033-C4"])
def check_contradiction(formalization: Formalization) -> ContradictionFinding | None:
    """Detect whether ``formalization``'s constraint set admits no solution.

    On unsatisfiability, computes an approximate-minimal unsatisfiable core
    via the standard deletion-based algorithm: walk the constraints in
    declaration order, tentatively drop each one, and keep the drop
    permanent only if the remaining set is STILL unsatisfiable (i.e. the
    dropped constraint wasn't needed to produce the contradiction). This is
    deterministic given the declaration order but not guaranteed to be the
    globally smallest unsatisfiable subset -- it is an approximation, as the
    B26 brief specifies.

    Returns:
        None if satisfiable; otherwise a :class:`ContradictionFinding` naming
        the conflicting constraint ids and their ``source`` provenance.
    """
    if _has_solution(formalization):
        return None

    core = list(formalization.constraints)
    index = 0
    while index < len(core):
        candidate = core[:index] + core[index + 1 :]
        candidate_formalization = dataclasses.replace(
            formalization, constraints=tuple(candidate)
        )
        if not _has_solution(candidate_formalization):
            # Dropping this constraint left the remainder unsatisfiable, so
            # it wasn't needed for the contradiction -- drop it for good.
            core = candidate
        else:
            # This constraint is necessary to the contradiction -- keep it.
            index += 1

    return ContradictionFinding(
        requirement_id=formalization.requirement_id,
        conflicting_constraint_ids=tuple(c.constraint_id for c in core),
        conflicting_sources=tuple(c.source for c in core),
    )


@traces(spec="033", reqs=["REQ-033-C4"])
def check_under_constraint(
    formalization: Formalization,
) -> UnderConstraintFinding | None:
    """Detect whether the observable projection of the solution set has >=2 members.

    Projects every solution onto its observable variables; if fewer than
    two distinct projections exist (0 solutions, or all solutions agree on
    every observable variable), the formalization is fully pinned and this
    returns None. A non-observable-only difference between solutions is NOT
    under-constraint -- materiality is defined over observable variables
    only (ADR-0022).

    Returns:
        None if fully pinned (or unsatisfiable); otherwise an
        :class:`UnderConstraintFinding` carrying two full concrete witness
        assignments and the observable variables on which they differ.
    """
    projections = _observable_projections(formalization)
    if len(projections) < 2:
        return None

    observable = _observable_names(formalization)
    (projection_a, witness_a), (projection_b, witness_b) = list(projections.items())[:2]
    differing = tuple(
        name
        for name, value_a, value_b in zip(
            observable, projection_a, projection_b, strict=True
        )
        if value_a != value_b
    )
    return UnderConstraintFinding(
        requirement_id=formalization.requirement_id,
        differing_observable_vars=differing,
        witness_a=dict(witness_a),
        witness_b=dict(witness_b),
    )


@traces(spec="033", reqs=["REQ-033-C4"])
def run_c4(formalization: Formalization) -> C4Report:
    """Run both C4 detectors over ``formalization`` and combine their results.

    ``solution_count_observable`` is the number of DISTINCT observable
    projections (0 if unsatisfiable, 1 if fully pinned, >=2 if
    under-constrained) -- not the raw solution count, which may be larger
    when non-observable variables vary freely.
    """
    contradiction = check_contradiction(formalization)
    under_constraint = check_under_constraint(formalization)
    solution_count_observable = (
        0 if contradiction is not None else len(_observable_projections(formalization))
    )
    return C4Report(
        requirement_id=formalization.requirement_id,
        contradiction=contradiction,
        under_constraint=under_constraint,
        solution_count_observable=solution_count_observable,
    )