0711988b67
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%.
36 lines
1.5 KiB
Python
36 lines
1.5 KiB
Python
"""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, ...]"
|