Merge pull request #746 from AssetOverflow/codex/m1-composition-plan-logic-parity

feat(composition): M1 — logic is-a chain → plan→lower→verify spine (byte-parity refactor)

generate/composition/__init__.py

@@ -0,0 +1,27 @@
+"""Compositional reading spine (plan -> lower -> verify).
+
+The comprehension organ recognizes individual structures but cannot COMPOSE them
+across a unit/structure/referent boundary — the proven coverage wall
+(``docs/analysis/comprehension-coverage-wall-map-2026-06-14.md``). This package is the
+fix: a deterministic stage that builds a typed composition *plan* from clause-local
+sub-structures, LOWERS it into a domain's existing proof object, and routes that object
+UNCHANGED through the domain's existing sound gate. The composition layer has zero
+authority to commit an answer — the unchanged, from-scratch re-deriving gate is the
+sole wrong=0 firewall.
+
+The spine is intended to be domain-general (one ``lower(plan) -> proof_object`` per
+domain, each over the same plan core), but **M1 ships the LOGIC instantiation only**:
+it generalizes the is-a chain previously inlined in
+``generate/determine/determine.py::_verify_subsumption`` into a reusable
+``LogicChainPlan`` + ``lower_logic_chain``, byte-identical to the original (a parity
+refactor — no new capability). The math instantiation (``lower_math_plan`` over a
+``GroundedDerivation``) and additional join-ops land in later phases, one op per PR,
+each behind a grounded case + a mutation test that the gate refuses a mis-licensed
+edge. Discipline: CLAUDE.md (Schema-Defined Proof Obligations,
+defer-substrate-vocab-commitment).
+"""
+
+from generate.composition.lower_logic import lower_logic_chain
+from generate.composition.plan import LogicChainPlan
+
+__all__ = ["LogicChainPlan", "lower_logic_chain"]

generate/composition/lower_logic.py

@@ -0,0 +1,85 @@
+"""Logic lowering — a ``LogicChainPlan`` becomes a propositional (premises, query)
+theory for the sound ROBDD gate. Extracted byte-identically from
+``generate/determine/determine.py::_verify_subsumption`` (M1 parity refactor).
+
+The lowering proposes a theory; it NEVER evaluates entailment. The caller routes the
+result through the UNCHANGED ``evaluate_entailment`` gate, which re-derives validity
+from scratch — so a path-construction bug here cannot produce a wrong assertion
+(soundness by construction).
+"""
+
+from __future__ import annotations
+
+from generate.composition.plan import LogicChainPlan
+
+
+def lower_logic_chain(plan: LogicChainPlan) -> tuple[tuple[str, ...], str] | None:
+    """Lower an is-a chain plan into a propositional ``(premises, query_atom)`` theory.
+
+    The propositional theory labels every ``subset_path`` fact ``S`` and the
+    ``member_fact`` ``M``, asserts each edge plus the sound rule that extends the chain
+    (``member ∘ subset → member`` / ``subset ∘ subset → subset``), and queries the
+    closure atom. It is LINEAR in the path (the facts as true atoms + the sound rule at
+    each hop), so it scales.
+
+    Returns ``None`` for a mislabeled or wrong-arity chain — refuse rather than smuggle
+    a ``member`` fact in as a ``subset`` edge (``member ∘ member`` cannot be laundered
+    through a corrupted path), rather than trust the callers' discipline.
+    """
+    predicate = plan.predicate
+    subject = plan.subject
+    target = plan.target
+    member_fact = plan.member_fact
+    subset_path = plan.subset_path
+
+    # Soundness-by-construction (belt-and-suspenders): refuse a mislabeled / wrong-arity
+    # chain here, so a corrupted path cannot verify a smuggled member fact as a subset
+    # edge regardless of either caller's discipline.
+    if member_fact is not None and (
+        member_fact.relation_predicate != "member"
+        or len(member_fact.relation_arguments) != 2
+    ):
+        return None
+    if any(
+        f.relation_predicate != "subset" or len(f.relation_arguments) != 2
+        for f in subset_path
+    ):
+        return None
+
+    atoms: dict[tuple[str, str, str], str] = {}
+
+    def atom(p: str, a: str, b: str) -> str:
+        key = (p, a, b)
+        name = atoms.get(key)
+        if name is None:
+            name = f"x{len(atoms)}"
+            atoms[key] = name
+        return name
+
+    premises: list[str] = []
+    # Walk the subset path, asserting each edge and the sound rule that extends the chain.
+    if predicate == "member":
+        assert member_fact is not None
+        cur = member_fact.relation_arguments[1]
+        premises.append(atom("M", subject, cur))  # member(subject, b) is told
+        for fact in subset_path:
+            nxt = fact.relation_arguments[1]
+            premises.append(atom("S", cur, nxt))  # subset(cur, nxt) is told
+            premises.append(  # member ∘ subset → member
+                f"({atom('M', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('M', subject, nxt)}"
+            )
+            cur = nxt
+        query_atom = atom("M", subject, target)
+    else:
+        cur = subject
+        for hop, fact in enumerate(subset_path):
+            nxt = fact.relation_arguments[1]
+            premises.append(atom("S", cur, nxt))  # subset(cur, nxt) is told
+            if hop > 0:  # the first told edge IS the accumulator S_subject_c1; extend it
+                premises.append(  # subset ∘ subset → subset
+                    f"({atom('S', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('S', subject, nxt)}"
+                )
+            cur = nxt
+        query_atom = atom("S", subject, target)
+
+    return tuple(premises), query_atom

generate/composition/plan.py

@@ -0,0 +1,36 @@
+"""Composition plan types — the typed structure a composer proposes (never commits).
+
+A plan binds clause-local sub-structures into one composite that the lowering turns
+into a domain proof object for an UNCHANGED sound gate. M1 lands only the logic is-a
+chain. A closed join-op vocabulary is deliberately NOT introduced yet
+(defer-substrate-vocab-commitment): the chain discriminates on the relational
+``predicate`` it already carries, and an explicit join-op field lands only when a
+second op's lowering actually dispatches on it (M3).
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:  # type-only — avoids any import cycle with the realize/determine path
+    from generate.realize import RealizedRecord
+
+
+@dataclass(frozen=True, slots=True)
+class LogicChainPlan:
+    """The logic instantiation of the plan -> lower -> verify spine: an is-a chain.
+
+    Carries the clause-local relational roots — an optional ``member`` fact plus an
+    ordered ``subset`` path. The plan proposes structure only; ``lower_logic_chain``
+    turns it into a propositional theory that an UNCHANGED sound gate
+    (``generate.proof_chain.entail.evaluate_entailment``) must accept. The plan never
+    decides truth. Generalizes the chain previously inlined in
+    ``generate/determine/determine.py::_verify_subsumption`` (byte-identical lowering).
+    """
+
+    predicate: str  # "member" | "subset"
+    subject: str
+    target: str
+    member_fact: "RealizedRecord | None"
+    subset_path: "tuple[RealizedRecord, ...]"

generate/determine/determine.py

@@ -31,6 +31,7 @@ from __future__ import annotations
 
 from dataclasses import dataclass
 
+from generate.composition import LogicChainPlan, lower_logic_chain
 from generate.meaning_graph.reader import Comprehension, Refusal
 from generate.meaning_graph.relational import RELATIONAL_PREDICATES
 from generate.realize import RealizedRecord, recall_realized
@@ -244,60 +245,23 @@ def _verify_subsumption(
     # Soundness-by-construction (belt-and-suspenders): the propositional theory below
     # labels every ``subset_path`` fact ``S`` and the ``member_fact`` ``M``. Both callers
     # (``_determine_subsumption`` and ``consolidate``) build these from predicate-filtered
-    # recalls, so the labels match — but the theory would otherwise verify a smuggled
-    # member fact in ``subset_path`` as a (potentially unsound) subset edge. Refuse a
-    # mislabeled or wrong-arity chain here rather than trust two callers' discipline, so
-    # ``member ∘ member`` cannot be laundered through a corrupted path.
-    if member_fact is not None and (
-        member_fact.relation_predicate != "member"
-        or len(member_fact.relation_arguments) != 2
-    ):
+    # recalls, so the labels match — the lowering refuses a mislabeled / wrong-arity
+    # chain (``member ∘ member`` cannot be laundered through a corrupted path).
+    plan = LogicChainPlan(
+        predicate=predicate,
+        subject=subject,
+        target=target,
+        member_fact=member_fact,
+        subset_path=subset_path,
+    )
+    lowered = lower_logic_chain(plan)
+    if lowered is None:
         return None
-    if any(
-        f.relation_predicate != "subset" or len(f.relation_arguments) != 2
-        for f in subset_path
-    ):
-        return None
-
-    atoms: dict[tuple[str, str, str], str] = {}
-
-    def atom(p: str, a: str, b: str) -> str:
-        key = (p, a, b)
-        name = atoms.get(key)
-        if name is None:
-            name = f"x{len(atoms)}"
-            atoms[key] = name
-        return name
-
-    premises: list[str] = []
-    # Walk the subset path, asserting each edge and the sound rule that extends the chain.
-    if predicate == "member":
-        assert member_fact is not None
-        cur = member_fact.relation_arguments[1]
-        premises.append(atom("M", subject, cur))  # member(subject, b) is told
-        for fact in subset_path:
-            nxt = fact.relation_arguments[1]
-            premises.append(atom("S", cur, nxt))  # subset(cur, nxt) is told
-            premises.append(  # member ∘ subset → member
-                f"({atom('M', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('M', subject, nxt)}"
-            )
-            cur = nxt
-        query_atom = atom("M", subject, target)
-    else:
-        cur = subject
-        for hop, fact in enumerate(subset_path):
-            nxt = fact.relation_arguments[1]
-            premises.append(atom("S", cur, nxt))  # subset(cur, nxt) is told
-            if hop > 0:  # the first told edge IS the accumulator S_subject_c1; extend it
-                premises.append(  # subset ∘ subset → subset
-                    f"({atom('S', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('S', subject, nxt)}"
-                )
-            cur = nxt
-        query_atom = atom("S", subject, target)
+    premises, query_atom = lowered
 
     from generate.proof_chain.entail import Entailment, evaluate_entailment
 
-    if evaluate_entailment(tuple(premises), query_atom).outcome is not Entailment.ENTAILED:
+    if evaluate_entailment(premises, query_atom).outcome is not Entailment.ENTAILED:
         return None
 
     grounds = ((member_fact,) if member_fact is not None else ()) + subset_path

tests/test_composition_lower_logic.py

@@ -0,0 +1,92 @@
+"""M1 — the composition spine's logic lowering, in isolation.
+
+`lower_logic_chain` is the extracted (byte-identical) lowering from
+`generate/determine/determine.py::_verify_subsumption`. These pin the EXACT
+propositional theory it emits (so a wrong extraction is caught) and the
+soundness-by-construction refusal of a mislabeled chain. The byte-PARITY of the
+end-to-end determine path is covered by the unchanged determine/transitive tests.
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+
+from generate.composition import LogicChainPlan, lower_logic_chain
+
+
+@dataclass(frozen=True)
+class _Fact:
+    """Minimal duck-typed relational fact (the lowering reads only these two)."""
+
+    relation_predicate: str
+    relation_arguments: tuple[str, ...]
+
+
+def test_member_chain_lowers_to_member_subset_theory() -> None:
+    # "Socrates is a man" (member) ∘ "man ⊆ mortal" (subset) → member(Socrates, mortal).
+    plan = LogicChainPlan(
+        predicate="member",
+        subject="socrates",
+        target="mortal",
+        member_fact=_Fact("member", ("socrates", "man")),
+        subset_path=(_Fact("subset", ("man", "mortal")),),
+    )
+    lowered = lower_logic_chain(plan)
+    assert lowered is not None
+    premises, query = lowered
+    # M(soc,man)=x0, S(man,mortal)=x1, sound rule (M∘S→M): (x0 & x1) -> M(soc,mortal)=x2.
+    assert premises == ("x0", "x1", "(x0 & x1) -> x2")
+    assert query == "x2"
+
+
+def test_subset_chain_lowers_to_subset_subset_theory() -> None:
+    # "a ⊆ b", "b ⊆ c" → subset(a, c) by subset ∘ subset.
+    plan = LogicChainPlan(
+        predicate="subset",
+        subject="a",
+        target="c",
+        member_fact=None,
+        subset_path=(_Fact("subset", ("a", "b")), _Fact("subset", ("b", "c"))),
+    )
+    lowered = lower_logic_chain(plan)
+    assert lowered is not None
+    premises, query = lowered
+    # S(a,b)=x0, S(b,c)=x1, rule (S∘S→S): (x0 & x1) -> S(a,c)=x2.
+    assert premises == ("x0", "x1", "(x0 & x1) -> x2")
+    assert query == "x2"
+
+
+def test_mislabeled_member_fact_refuses() -> None:
+    # A member_fact whose predicate is not "member" must NOT be lowered (it could be
+    # smuggled in as a subset edge → an unsound member∘member chain).
+    plan = LogicChainPlan(
+        predicate="member",
+        subject="socrates",
+        target="mortal",
+        member_fact=_Fact("subset", ("socrates", "man")),  # wrong predicate
+        subset_path=(_Fact("subset", ("man", "mortal")),),
+    )
+    assert lower_logic_chain(plan) is None
+
+
+def test_member_fact_in_subset_path_refuses() -> None:
+    # A "member" fact laundered into the subset_path must be refused.
+    plan = LogicChainPlan(
+        predicate="subset",
+        subject="a",
+        target="c",
+        member_fact=None,
+        subset_path=(_Fact("subset", ("a", "b")), _Fact("member", ("b", "c"))),  # member smuggled in
+    )
+    assert lower_logic_chain(plan) is None
+
+
+def test_wrong_arity_refuses() -> None:
+    plan = LogicChainPlan(
+        predicate="subset",
+        subject="a",
+        target="c",
+        member_fact=None,
+        subset_path=(_Fact("subset", ("a", "b", "extra")),),  # arity 3
+    )
+    assert lower_logic_chain(plan) is None