Merge pull request #555 from AssetOverflow/feat/phase1-universal-structure
Phase 1 — canonize binding-graph interlingua + INV-26 neutrality
This commit is contained in:
commit
4d964020a9
3 changed files with 193 additions and 2 deletions
|
|
@ -137,7 +137,9 @@ genuine second derivation. Cannot → we learned it cheaply and honestly.
|
|||
gold. Gate to everything geometric.
|
||||
- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding
|
||||
first), with **field ⟂ symbol agreement** as the admission gate from the moment
|
||||
Phase 1.5 succeeds.
|
||||
Phase 1.5 succeeds. **The diversity panel starts here** (see cross-cutting): the
|
||||
compiler is validated against ≥2 structurally-distinct golded domains from its
|
||||
first commit, so it cannot overfit to math-shaped problems.
|
||||
- **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2
|
||||
signal; wire the propose-loop consuming `checker="t2_precision"`. No invented
|
||||
second derivation needed — it is real now.
|
||||
|
|
@ -152,7 +154,35 @@ genuine second derivation. Cannot → we learned it cheaply and honestly.
|
|||
modality becomes "just another reader" grounding into the universal structure;
|
||||
stays afferent/gated per ADR-0198.
|
||||
|
||||
### Cross-cutting (every phase) — checkable budgets, adjoints, phenomenology
|
||||
### Cross-cutting (every phase) — diversity panel, checkable budgets, adjoints, phenomenology
|
||||
|
||||
- **Structurally-diverse checkable panel (the anti-overfit instrument) — woven in
|
||||
from Phase 2, not deferred to Phase 5.** Multi-domain diversity is not a morale
|
||||
tool bolted onto the plan; it *is* the experiment that confirms or refutes the
|
||||
central thesis (that *different* subjects compile into the *same* universal
|
||||
structure and are handled by the *same* solve/verify machinery). The defining
|
||||
failure of this project was a single gameable ruler (the 50-case train_sample)
|
||||
hiding unsoundness for weeks; the antidote is a panel of **structurally distinct**
|
||||
domains, each with a **genuine independent gold** (the INV-25 bar — a verifier
|
||||
sharing no code with the engine). Adding a domain *without* real independent gold
|
||||
is worse than useless: it is another gameable ruler. The cheap, strong starting
|
||||
panel (logic / grounding / dimensional / execution / constraint, all with real
|
||||
gold):
|
||||
- **deductive logic** (ROBDD vs. truth-table oracle) — shipped.
|
||||
- **finite-entity grounding** (ROBDD/oracle gold; Phase 2).
|
||||
- **units / dimensional analysis** — *nearly free*: the binding graph already
|
||||
carries dimensional algebra, so "does the answer's dimension check out" is an
|
||||
independent structural gold.
|
||||
- **systems/software** (execution = gold; Phase 5) — the strongest verifier.
|
||||
- **a small constraint/scheduling domain** (brute-force/SMT gold).
|
||||
|
||||
**The discipline (adopt now):** *a capability change must move ≥2 structurally-
|
||||
distinct domains, or it is suspected overfitting until proven otherwise.* Make the
|
||||
panel a first-class CI signal alongside GSM8K so progress is never read from one
|
||||
flat number. Honesty note: a domain with no adequate pack yet simply refuses
|
||||
everything — that is a *coverage* signal (a breadth map), not a *capability*
|
||||
signal. Capability credit counts only where there is a real pack **and** a real
|
||||
gold **and** committed (non-refused) agreement.
|
||||
|
||||
- **Distortion budgets as first-class CI gates**, but *only checkable ones*:
|
||||
grounding completeness %, unit-proof coverage, acyclicity, and **structural
|
||||
|
|
|
|||
|
|
@ -1,5 +1,24 @@
|
|||
"""ADR-0132/0133/0134/0135 — Semantic-Symbolic Binding Graph.
|
||||
|
||||
**The universal problem-structure interlingua** (see
|
||||
``docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md``).
|
||||
This is the one typed, field-agnostic structure that every reader (math,
|
||||
deductive logic, future modalities) compiles *into* and every solver/verifier
|
||||
operates *on*: a unit-aware, provenance-carrying (:class:`SourceSpanLink`),
|
||||
acyclic, refusal-first DAG. It is the corpus callosum where holistic
|
||||
comprehension commits to an inspectable, checkable form and hands off to
|
||||
analysis — not the master and not a mere servant.
|
||||
|
||||
**Neutrality doctrine (enforced by INV-26).** The interlingua must depend on
|
||||
neither the field engine, nor any one domain's reader, nor the eval/runtime: the
|
||||
core model imports nothing from ``field`` / ``algebra`` / ``evals`` / ``vault`` /
|
||||
``chat``, and only the designated *bridge* modules (:mod:`.adapter`,
|
||||
:mod:`.question_target`) may import a domain reader. Servants propose into the
|
||||
structure and check it; they never become the structure. Keeping the meeting
|
||||
point neutral is what lets two independent decodings (geometric field and
|
||||
symbolic ROBDD) agree *here* — the coherence that makes a committed answer
|
||||
``wrong == 0``-safe.
|
||||
|
||||
Phase 1 (ADR-0132): pure data layer (frozen dataclasses, deterministic
|
||||
allocator, refusal-first construction; no I/O, no parser, no algebra,
|
||||
no ``Polynomial`` coupling — symbolic expressions held as canonical
|
||||
|
|
|
|||
|
|
@ -1242,3 +1242,145 @@ class TestINV25IndependentGold:
|
|||
"entailed/refuted signal, so INV-25b cannot catch a soundness break. "
|
||||
"Add non-trivial cases before claiming the lane proves capability."
|
||||
)
|
||||
|
||||
|
||||
# ===========================================================================
|
||||
# INV-26 Interlingua neutrality — the universal problem-structure does not
|
||||
# depend on the field engine, any one domain reader, or eval/runtime
|
||||
# ===========================================================================
|
||||
#
|
||||
# Claim (docs/analysis/universal-structure-and-field-symbol-coherence-gate-
|
||||
# 2026-06-04.md §2; ADR-0132 "no algebra" rule made structural):
|
||||
#
|
||||
# The binding graph is the corpus callosum where two independent decodings
|
||||
# (the geometric field and the symbolic ROBDD) must be able to meet and
|
||||
# AGREE. That is only sound if the meeting point is NEUTRAL: if the
|
||||
# interlingua imported the field engine, a benchmark, or a single domain's
|
||||
# reader, "agreement at the interlingua" would be agreement-with-oneself —
|
||||
# the same blind spot INV-25 guards for gold. So:
|
||||
#
|
||||
# 26a No binding-graph module imports the field engine, eval, vault, or the
|
||||
# runtime (``field`` / ``algebra`` / ``evals`` / ``vault`` / ``chat`` /
|
||||
# ``core`` / ``sensorium``). The structure is engine/benchmark/runtime-
|
||||
# neutral.
|
||||
# 26b The binding-graph CORE (everything but the allowlisted bridge modules)
|
||||
# imports nothing outside the standard library and its own package —
|
||||
# in particular no domain reader. Only the bridges (``adapter``,
|
||||
# ``question_target``) may translate a domain reader into the structure.
|
||||
# 26c Non-vacuity: a module that imports a forbidden family is shown to be
|
||||
# flagged, proving 26a/26b can fail.
|
||||
#
|
||||
# A new bridge (a new domain reader translated into the structure) is allowed,
|
||||
# but must be added to BINDING_GRAPH_BRIDGES explicitly — that is the reviewable
|
||||
# seam where a domain couples to the universal structure.
|
||||
|
||||
_BINDING_GRAPH_DIR = "generate/binding_graph"
|
||||
|
||||
# Engine / benchmark / runtime families the interlingua must never import.
|
||||
_INTERLINGUA_FORBIDDEN_PREFIXES: tuple[str, ...] = (
|
||||
"field", "algebra", "evals", "vault", "chat", "core", "sensorium",
|
||||
)
|
||||
|
||||
# The only modules permitted to import a domain reader (they translate one
|
||||
# domain's reader output into the neutral structure).
|
||||
BINDING_GRAPH_BRIDGES: frozenset[str] = frozenset({
|
||||
"adapter.py",
|
||||
"question_target.py",
|
||||
})
|
||||
|
||||
|
||||
def _binding_graph_modules() -> list[Path]:
|
||||
return sorted((_REPO_ROOT / _BINDING_GRAPH_DIR).glob("*.py"))
|
||||
|
||||
|
||||
def _is_internal_or_stdlib(mod: str) -> bool:
|
||||
"""True if an imported module name is the structure's own package."""
|
||||
return mod == "generate.binding_graph" or mod.startswith("generate.binding_graph.")
|
||||
|
||||
|
||||
class TestINV26InterlinguaNeutrality:
|
||||
"""The universal problem-structure stays neutral to engine, benchmark, and
|
||||
runtime, and its core depends on no single domain reader."""
|
||||
|
||||
def test_binding_graph_dir_exists(self):
|
||||
mods = _binding_graph_modules()
|
||||
assert mods, (
|
||||
f"no binding-graph modules found under {_BINDING_GRAPH_DIR} — "
|
||||
"INV-26 would be vacuous (did the package move?)."
|
||||
)
|
||||
|
||||
def test_no_module_imports_engine_eval_or_runtime(self):
|
||||
"""26a — the interlingua never touches field/algebra/eval/vault/chat/
|
||||
core/sensorium. Agreement at a neutral meeting point is real; agreement
|
||||
at a point coupled to one engine is agreement-with-oneself."""
|
||||
offenders: list[str] = []
|
||||
for path in _binding_graph_modules():
|
||||
mods = _module_imports(path)
|
||||
hits = _imports_any_prefix(mods, _INTERLINGUA_FORBIDDEN_PREFIXES)
|
||||
if hits:
|
||||
offenders.append(f"{path.name} imports {hits}")
|
||||
assert not offenders, (
|
||||
"Binding-graph (interlingua) module couples to the engine/eval/"
|
||||
"runtime:\n " + "\n ".join(offenders)
|
||||
+ "\n\nThe universal structure must stay neutral so two independent "
|
||||
"decodings can meet and agree there (INV-26a). Move the coupling out, "
|
||||
"or it is not an interlingua."
|
||||
)
|
||||
|
||||
def test_core_imports_no_domain_reader(self):
|
||||
"""26b — only the allowlisted bridges may import a domain reader; the
|
||||
core imports nothing outside stdlib + its own package."""
|
||||
offenders: list[str] = []
|
||||
for path in _binding_graph_modules():
|
||||
if path.name in BINDING_GRAPH_BRIDGES or path.name == "__init__.py":
|
||||
continue
|
||||
external = [
|
||||
m for m in _module_imports(path)
|
||||
if m.startswith("generate.") and not _is_internal_or_stdlib(m)
|
||||
]
|
||||
if external:
|
||||
offenders.append(f"{path.name} imports domain module(s) {sorted(external)}")
|
||||
assert not offenders, (
|
||||
"Binding-graph CORE imports a domain reader (couples the universal "
|
||||
"structure to one domain):\n " + "\n ".join(offenders)
|
||||
+ "\n\nTranslate the domain via a bridge module and add it to "
|
||||
"BINDING_GRAPH_BRIDGES, or keep the core domain-agnostic (INV-26b)."
|
||||
)
|
||||
|
||||
def test_bridges_exist_and_are_used(self):
|
||||
"""Drift guard: every allowlisted bridge must exist and actually import a
|
||||
domain reader, else the allowlist is stale and 26b is weakened."""
|
||||
present = {p.name for p in _binding_graph_modules()}
|
||||
missing = BINDING_GRAPH_BRIDGES - present
|
||||
assert not missing, f"BINDING_GRAPH_BRIDGES names non-existent module(s): {missing}"
|
||||
unused: list[str] = []
|
||||
for name in sorted(BINDING_GRAPH_BRIDGES):
|
||||
mods = _module_imports(_REPO_ROOT / _BINDING_GRAPH_DIR / name)
|
||||
if not any(m.startswith("generate.") and not _is_internal_or_stdlib(m) for m in mods):
|
||||
unused.append(name)
|
||||
assert not unused, (
|
||||
f"Allowlisted bridge(s) no longer import a domain reader: {unused}. "
|
||||
"Remove from BINDING_GRAPH_BRIDGES to keep the coupling seam tight."
|
||||
)
|
||||
|
||||
def test_neutrality_check_is_non_vacuous(self):
|
||||
"""26c — prove 26a/26b can fail: a real module that imports a forbidden
|
||||
family must be flagged by the same predicate."""
|
||||
# core/cognition/pipeline.py imports field.state (engine) — 26a must flag it.
|
||||
pipeline = _REPO_ROOT / "core" / "cognition" / "pipeline.py"
|
||||
if pipeline.is_file():
|
||||
hits = _imports_any_prefix(_module_imports(pipeline), _INTERLINGUA_FORBIDDEN_PREFIXES)
|
||||
assert hits, (
|
||||
"INV-26a predicate failed to flag a module known to import the "
|
||||
"field engine — the neutrality check is vacuous."
|
||||
)
|
||||
# The bridge adapter imports a domain reader — 26b's predicate must see it.
|
||||
adapter = _REPO_ROOT / _BINDING_GRAPH_DIR / "adapter.py"
|
||||
external = [
|
||||
m for m in _module_imports(adapter)
|
||||
if m.startswith("generate.") and not _is_internal_or_stdlib(m)
|
||||
]
|
||||
assert external, (
|
||||
"INV-26b predicate failed to detect the adapter's domain-reader "
|
||||
"import — the core-isolation check is vacuous."
|
||||
)
|
||||
|
|
|
|||
Loading…
Reference in a new issue