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 |
|