From 0711988b670a6deb3b8200f54f8815c0b10045d8 Mon Sep 17 00:00:00 2001 From: Shay Date: Sun, 14 Jun 2026 15:42:24 -0700 Subject: [PATCH] =?UTF-8?q?feat(composition):=20M1=20=E2=80=94=20extract?= =?UTF-8?q?=20the=20logic=20is-a=20chain=20into=20a=20plan->lower->verify?= =?UTF-8?q?=20spine=20(byte-parity)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First phase of the domain-general compositional reading layer (the comprehension coverage wall is composition — docs/analysis/comprehension-coverage-wall-map-2026-06-14.md). M1 is a pure PARITY refactor on the flagship logic path, no new capability: - new generate/composition/ package: LogicChainPlan (plan.py) + lower_logic_chain (lower_logic.py), the is-a chain lowering extracted BYTE-IDENTICALLY from determine.py::_verify_subsumption. - _verify_subsumption now builds a plan -> lowers it -> routes through the UNCHANGED evaluate_entailment gate. The composer proposes structure; the sound ROBDD gate remains the sole wrong=0 firewall. - only the logic instantiation ships; no math lowering, no join-op vocabulary (defer-substrate-vocab-commitment — the chain discriminates on its relational predicate, an explicit join-op field lands when a second op dispatches on it). Verification: byte-identical lowering (3-reviewer adversarial panel: byte-parity PASS char-for-char, wrong=0 PASS — the instance-of-fallacy refusal mutation-proven load-bearing); 5 new non-vacuous lowering tests; 28 determine/transitive/consolidation + 163-test broad sweep (incl. gsm8k serving + ADR-0218) green; cognition eval 100%. --- generate/composition/__init__.py | 27 ++++++++ generate/composition/lower_logic.py | 85 +++++++++++++++++++++++++ generate/composition/plan.py | 36 +++++++++++ generate/determine/determine.py | 64 ++++--------------- tests/test_composition_lower_logic.py | 92 +++++++++++++++++++++++++++ 5 files changed, 254 insertions(+), 50 deletions(-) create mode 100644 generate/composition/__init__.py create mode 100644 generate/composition/lower_logic.py create mode 100644 generate/composition/plan.py create mode 100644 tests/test_composition_lower_logic.py diff --git a/generate/composition/__init__.py b/generate/composition/__init__.py new file mode 100644 index 00000000..16ec8f5e --- /dev/null +++ b/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"] diff --git a/generate/composition/lower_logic.py b/generate/composition/lower_logic.py new file mode 100644 index 00000000..22abf582 --- /dev/null +++ b/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 diff --git a/generate/composition/plan.py b/generate/composition/plan.py new file mode 100644 index 00000000..6c9d5756 --- /dev/null +++ b/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, ...]" diff --git a/generate/determine/determine.py b/generate/determine/determine.py index ceb0a402..4e1df8d6 100644 --- a/generate/determine/determine.py +++ b/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 diff --git a/tests/test_composition_lower_logic.py b/tests/test_composition_lower_logic.py new file mode 100644 index 00000000..d50690f9 --- /dev/null +++ b/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