core-labs/core - Forgejo: Beyond coding. We forge.

core-labs/core

Fork 0

Commit graph

Author	SHA1	Message	Date
Shay	69a7d8bae8	feat: principled out-of-regime detector — typed out_of_decidable_regime (ADR-0201.1) GPT-5.5's independent corpus caught that the canonicalizer refused quantified/ predicate input only by accident (tokenizer chokes on '.'), not by design — a by-luck-not-by-design refusal the wrong=0 discipline rejects. ADR-0202 §3 names a typed `out_of_decidable_regime` refusal; the keystone emitted a generic grammar error. - logic_canonical.py: LogicRegimeError(LogicError) + OUT_OF_DECIDABLE_REGIME; _reject_out_of_regime_text (quantifier words forall/exists + symbols ∀/∃, pre-scan) and _reject_out_of_regime_tokens (predicate-application ATOM-then-LPAREN), run BEFORE the generic grammar error. Refusal only — no predicate/FOL capability added. - logic_equivalence.py: typed regime branch (before the generic LogicError branch). - tests: 43 total (10 new) — OOR refuses with typed reason; equivalence path too; genuine grammar errors stay plain LogicError (no over-fire); `not (P)` not mistaken for predicate application. Mutation-verified by-design (neuter -> falls through to generic grammar error). - ADR-0201.1: additive sub-ADR of 0201 (not an amendment; sub-number preserves the landed ADR-0203 forward refs + phase-2 plan numbering). Honesty boundary load-bearing. Corpus now 22/22 (PC-OOR-001/002 agree on the principled reason). Full canonicalizer suite green; smoke 67 passed. modus_ponens rule-reasons remain deferred to ADR-0205 (2.3).	2026-06-02 19:12:41 -07:00
Shay	e8e0fbb014	feat: propositional canonicalizer keystone + representation contract (ADR-0201/0202) The proof_chain keystone: a hand-rolled ROBDD canonicalizer mirroring math_symbolic_equivalence one domain over (normalize -> canonical key -> byte-equality -> three-valued verdict; REFUSED preserves wrong=0). - generate/logic_canonical.py: formula -> ROBDD identity under sorted-atom ordering; LogicError/LogicBudgetError refusals; inspectable canonical key. - generate/logic_equivalence.py: EQUIVALENT/NOT_EQUIVALENT/REFUSED wrapper. - tests/test_logic_canonical.py: 33 standalone tests (canonicity laws, discrimination, terminals, determinism, refusals); mutation-verified non-vacuous. - ADR-0201: canonicalizer decision (ROBDD not CNF/DNF; hand-rolled; propositional-only honesty boundary). - ADR-0202: proposition representation contract — single source the canonicalizer and the proof corpus conform to (formula grammar + atom layer binding to ADR-0144 EpistemicNode + honesty boundary). Additive: no existing file touched, zero consumers. Standalone keystone only; binding-graph wiring, acyclicity refusal, and inference rules deferred. smoke: 67 passed.	2026-06-02 16:24:32 -07:00

Author

SHA1

Message

Date

Shay

69a7d8bae8

feat: principled out-of-regime detector — typed out_of_decidable_regime (ADR-0201.1)

GPT-5.5's independent corpus caught that the canonicalizer refused quantified/
predicate input only by accident (tokenizer chokes on '.'), not by design — a
by-luck-not-by-design refusal the wrong=0 discipline rejects. ADR-0202 §3 names a
typed `out_of_decidable_regime` refusal; the keystone emitted a generic grammar error.

- logic_canonical.py: LogicRegimeError(LogicError) + OUT_OF_DECIDABLE_REGIME;
  _reject_out_of_regime_text (quantifier words forall/exists + symbols ∀/∃, pre-scan)
  and _reject_out_of_regime_tokens (predicate-application ATOM-then-LPAREN), run BEFORE
  the generic grammar error. Refusal only — no predicate/FOL capability added.
- logic_equivalence.py: typed regime branch (before the generic LogicError branch).
- tests: 43 total (10 new) — OOR refuses with typed reason; equivalence path too;
  genuine grammar errors stay plain LogicError (no over-fire); `not (P)` not mistaken
  for predicate application. Mutation-verified by-design (neuter -> falls through to
  generic grammar error).
- ADR-0201.1: additive sub-ADR of 0201 (not an amendment; sub-number preserves the
  landed ADR-0203 forward refs + phase-2 plan numbering). Honesty boundary load-bearing.

Corpus now 22/22 (PC-OOR-001/002 agree on the principled reason). Full canonicalizer
suite green; smoke 67 passed. modus_ponens rule-reasons remain deferred to ADR-0205 (2.3).

2026-06-02 19:12:41 -07:00

Shay

e8e0fbb014

feat: propositional canonicalizer keystone + representation contract (ADR-0201/0202)

The proof_chain keystone: a hand-rolled ROBDD canonicalizer mirroring
math_symbolic_equivalence one domain over (normalize -> canonical key ->
byte-equality -> three-valued verdict; REFUSED preserves wrong=0).

- generate/logic_canonical.py: formula -> ROBDD identity under sorted-atom
  ordering; LogicError/LogicBudgetError refusals; inspectable canonical key.
- generate/logic_equivalence.py: EQUIVALENT/NOT_EQUIVALENT/REFUSED wrapper.
- tests/test_logic_canonical.py: 33 standalone tests (canonicity laws,
  discrimination, terminals, determinism, refusals); mutation-verified non-vacuous.
- ADR-0201: canonicalizer decision (ROBDD not CNF/DNF; hand-rolled;
  propositional-only honesty boundary).
- ADR-0202: proposition representation contract — single source the canonicalizer
  and the proof corpus conform to (formula grammar + atom layer binding to ADR-0144
  EpistemicNode + honesty boundary).

Additive: no existing file touched, zero consumers. Standalone keystone only;
binding-graph wiring, acyclicity refusal, and inference rules deferred. smoke: 67 passed.

2026-06-02 16:24:32 -07:00

2 commits