From 15307ca1f31edefa82bea9fef9ea9bebf6cc8b47 Mon Sep 17 00:00:00 2001 From: Shay Date: Tue, 2 Jun 2026 19:26:46 -0700 Subject: [PATCH] Add proof-chain corpus fixtures --- .../research/robdd_proof_chain_design_note.md | 229 ++++++ tests/fixtures/proof_chain/README.md | 57 ++ .../proof_chain/propositional_cases.json | 737 ++++++++++++++++++ 3 files changed, 1023 insertions(+) create mode 100644 docs/research/robdd_proof_chain_design_note.md create mode 100644 tests/fixtures/proof_chain/README.md create mode 100644 tests/fixtures/proof_chain/propositional_cases.json diff --git a/docs/research/robdd_proof_chain_design_note.md b/docs/research/robdd_proof_chain_design_note.md new file mode 100644 index 00000000..6ad1e7b8 --- /dev/null +++ b/docs/research/robdd_proof_chain_design_note.md @@ -0,0 +1,229 @@ +# ROBDD Proof-Chain Design Note + +**Status:** research note; reconciled with ADR-0201 / ADR-0202 +**Scope:** propositional canonicalizer and proof-corpus design support +**Date:** 2026-06-02 + +This note is syntax-independent at the proof-corpus level, but the formula +grammar and atom contract are now fixed by ADR-0202. The canonicalizer internals +and canonical-key string are fixed by ADR-0201. Proof-chain DAG wiring and +inference-rule result objects remain future work. + +## Executive Shape + +Reduced ordered binary decision diagrams (ROBDDs) are a good fit for the +propositional proof-chain keystone because they make the intrinsic space of a +proposition explicit: a Boolean function over a fixed ordered variable space. +Within that space, equivalence is structural identity, not a rewrite guess. + +The honesty boundary is just as important: this applies to propositional logic +under a fixed variable ordering. It does not transfer to predicate logic, +quantifiers, ungrounded propositions, or proof graphs with circular dependency. +Those cases should refuse with typed reasons rather than approximate. + +## Minimal Hand-Rolled Requirements + +A minimal ROBDD manager needs these pieces: + +- Two terminal leaves, `FALSE` and `TRUE`, represented by stable identities. +- Nonterminal nodes with `(variable, low, high)` where `low` is the branch for + the variable being false and `high` is the branch for true. +- A fixed variable order shared by every proposition compared in the same + equivalence domain. +- A `mk(variable, low, high)` constructor that is the only way to build + nonterminal nodes. +- A unique table keyed by `(variable, low_id, high_id)`. +- A computed cache keyed by `(operator, left_id, right_id)` for binary `apply`. + +The reduction rules are the load-bearing laws: + +1. Eliminate redundant tests: if `low == high`, return the child. +2. Merge isomorphic subgraphs: if another node has the same variable and + children, return the existing node identity. + +When these are enforced by `mk` and the variable order is fixed, a shared ROBDD +manager gives a strong canonical form: two represented functions are equivalent +iff their reduced diagrams are isomorphic. ADR-0201 exposes that identity as a +byte-deterministic structural `canonical_key` string, with tautology serialized +as `T` and contradiction serialized as `F`. + +## Apply Algorithm + +The core construction operator is `apply(op, left, right)`. + +At each recursive step: + +1. Return from the computed cache if `(op, left, right)` was already solved. +2. Apply terminal identities when both inputs are leaves, and simple short-cuts + where the selected operator permits them. +3. Select the topmost variable among the two input roots under the fixed order. +4. Recur on the low cofactors and high cofactors for that variable. +5. Reconstruct through `mk(top_variable, low_result, high_result)`. +6. Cache and return the resulting node. + +This is propagation through the Boolean function manifold, with `mk` as the +corrective conjugate that collapses redundant or duplicated structure on the way +back up. The resulting identity is not a syntactic normal form; it is the +reduced function itself, shared in the manager. + +## Variable Ordering + +Variable ordering is not a cosmetic choice. ROBDD size can vary sharply across +orders, and finding an optimal ordering is itself hard. CORE should therefore +treat ordering as a deterministic contract, not an optimization contest. + +For the small proof-step regime, the simplest adequate policy is: + +- derive the variable set from declared proposition atoms, +- reject ungrounded variables before construction, +- sort by the ADR-0202 atom id, +- freeze that order for all propositions in a comparison or proof step. + +Alternative local heuristics can be considered later only if they remain +byte-deterministic and are replayed as part of the trace. ADR-0201 chooses the +simplest v1 policy: atoms appearing in the formula, sorted lexicographically. + +The important constraint is that two propositions being compared must be built +in the same manager ordering. Different orders can represent the same Boolean +function with different graph identities, so ordering must be part of the +canonicalization domain. + +## Budget and Blowup Guard + +Bryant's original framing is the right discipline for CORE: many practical +Boolean functions compact well, but worst-case exponential growth remains real. +The canonicalizer should therefore have an explicit budget guard, not an +implicit timeout. + +Candidate budget dimensions: + +- maximum variable count, +- maximum created node count, +- maximum recursive `apply` calls, +- maximum computed-cache entries, +- maximum parse/AST depth before ROBDD construction, +- maximum proof-DAG node count for proof-chain validation. + +When a bound trips, the result should be the ADR-0202 typed refusal +`canonicalization_budget_exceeded`. It should not return a partial +canonical key, fall back to CNF/DNF, stochastic sampling, truth-table truncation, +or syntactic equality. Refusal preserves `wrong == 0`; churning or guessing does +not. + +The budget should be part of replay evidence. A refusal is only useful if the +trace can say which bound tripped and at what count. That lets future work tune +the construction boundary from evidence without changing the logical verdict of +any completed case. + +## Complement Edges + +Complement edges are optional for a first implementation. They can reduce memory +by encoding negation as a bit on an edge or pointer instead of constructing a +separate complemented graph. Mature packages use this technique, but it raises +implementation obligations: + +- regularize node pointers before unique-table lookup, +- define whether external root identity includes a complement mark, +- apply De Morgan transformations carefully in internal constructors, +- keep serialization byte-stable despite pointer-like internal representation. + +For CORE v1, plain nodes are easier to audit. Complement edges become attractive +only if node pressure is observed under replayable benchmark evidence. + +## Library vs Hand-Rolled + +ADR-0201 chose the hand-rolled path. The tradeoff remains useful context for why +that choice fits the proof-step regime. + +### Mature Library Path + +CUDD-style packages are battle-tested. They provide unique tables, computed +caches, garbage collection, complement edges, dynamic variable reordering, and a +large operation set. That is the strongest argument for using a mature library: +the difficult low-level machinery has already been exercised by verification +workloads. + +The cost is that such a dependency is heavy relative to the proof-step target: +opaque memory management, platform/build friction, optional dynamic reordering, +pointer-level identities, and many features CORE does not need for a small, +deterministic propositional corridor. If node identity is the canonical key, +library behavior must be constrained enough that replay is byte-stable. + +### Minimal Hand-Rolled Path + +A hand-rolled ROBDD manager is more work, but the v1 surface is compact: +terminal leaves, `mk`, unique table, computed cache, fixed variable ordering, +and `apply` for `not`, `and`, `or`, `implies`, and equivalence checking. + +This path fits CORE's character when the proposition regime is deliberately +small: inspectable, deterministic, local, and easy to refuse when budgets trip. +The risk is underestimating edge cases in hash-consing, ordering, cache +invalidity, serialization, or proof-DAG interaction. Those risks should be paid +down with an independent corpus and explicit refusal tests, not hidden by broad +fallbacks. + +## Proof-Chain Boundary + +ROBDD identity proves truth-functional equivalence. It does not, by itself, +prove that a submitted proof chain is valid. The proof-chain layer still needs +its own structural checks: + +- every referenced dependency must exist and be grounded, +- the dependency graph must be acyclic, +- each inference rule must declare the propositions it consumes, +- the derived proposition must be checked by the canonicalizer under the same + variable-order domain, +- out-of-regime formulas must refuse before canonical-key comparison. + +The first `modus_ponens` rule can be framed as a small entailment check: +dependencies contain an antecedent and a matching implication; the proposed +conclusion must match the implication's consequent in the ADR-0202 formula +representation. Future proof-chain wiring still needs to choose whether this is +implemented by syntactic pattern over parsed formula nodes, by ROBDD entailment, +or by a narrow rule object that delegates equivalence checks to the canonicalizer. + +## Validation Corpus Consequences + +The independent corpus should test behavior, not implementation internals. It +should therefore include: + +- equivalence pairs that force real Boolean canonicalization rather than shallow + operand sorting, +- non-equivalence near misses that catch over-collapse, +- TRUE/FALSE terminal reductions, +- valid and invalid `modus_ponens` examples, +- circular proof-DAG refusal, +- quantified/predicate out-of-regime refusal, +- budget-exceeded refusal for a scalable family. + +The corpus does not assert concrete node numbers. It asserts +equality/difference of `canonical_key`, typed terminal identity (`T` / `F`), and +typed refusals under the ADR-0202 atom and formula contract. + +## Confirmed Contract Points + +- Formula representation: ADR-0202 grammar over declared atom ids. +- Atom grounding: per-case atoms declare `gloss` and either + `binding.features` for intended ADR-0144/ADR-0143 FeatureBundle matching or + `binding: null` for schematic atoms. +- Variable ordering: lexicographic sorted atoms appearing in the formula. +- Canonical key: ADR-0201 byte-deterministic structural string; `T` and `F` for + terminal constants. +- Budget refusal: `canonicalization_budget_exceeded`. +- Complement edges: out of v1; ADR-0201 shipped a plain hand-rolled ROBDD. +- Still future proof-chain work: proof-DAG dependency object, circularity + checker, and concrete inference-rule result object. + +## Sources + +- Randal E. Bryant, "Graph-Based Algorithms for Boolean Function + Manipulation," IEEE Transactions on Computers, C-35:8, 1986. + https://doi.org/10.1109/TC.1986.1676819 +- Randal E. Bryant, "Binary Decision Diagrams: An Algorithmic Basis for + Symbolic Model Checking," 2018 chapter draft. + https://www.cs.cmu.edu/~bryant/pubdir/hmc-bdd18.pdf +- Fabio Somenzi, CUDD Programmer's Manual, release 2.5.0. + https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/ +- Seiichiro Tani, Kiyoharu Hamaguchi, and Shuzo Yajima, "The complexity of the + optimal variable ordering problems of shared binary decision diagrams," + ISAAC 1993. https://doi.org/10.1007/3-540-57568-5_270 diff --git a/tests/fixtures/proof_chain/README.md b/tests/fixtures/proof_chain/README.md new file mode 100644 index 00000000..4309b161 --- /dev/null +++ b/tests/fixtures/proof_chain/README.md @@ -0,0 +1,57 @@ +# Proof-Chain Fixture Scaffold + +**Status:** ADR-0202 grammar filled; not wired into the live suite +**Scope:** data-only fixture scaffold; not wired into the live test suite + +This directory is the independent validation scaffold for the propositional +canonicalizer and first `modus_ponens` proof-chain rule. The formula grammar, +atom declaration shape, and atom-to-FeatureBundle binding convention are governed +by `docs/decisions/ADR-0202-proposition-representation-contract.md`. + +The fixture inventory in `propositional_cases.json` records concrete formula +strings, per-case `atoms` blocks, expected behaviors, and rationale. It is ready +for a future proof-chain harness to wire, but it is intentionally not part of the +live test suite yet. + +## Atom Bindings + +Where a case atom maps to a recognizable fact, the atom records the intended +ADR-0144/ADR-0143 `FeatureBundle` binding as `binding.features`. The corpus does +not author `EpistemicNode.node_id`; that is assigned at recognition time. +Schematic budget atoms use `binding: null`. + +## Validation Boundaries + +The three `modus_ponens` cases are validated at entailment only. Their typed rule +reasons (`conclusion_mismatch` / `missing_implication`) are marked pending phase +2.3 / ADR-0205, when the rule checker lands. + +The two out-of-regime cases assert `out_of_decidable_regime` and record that this +is the `LogicRegimeError` reason produced by merged main after ADR-0201.1. + +## Required Categories + +- `equivalent_key`: propositions that must reduce to identical canonical keys. +- `different_key`: near-miss propositions that must not collapse. +- `tautology_or_contradiction`: formulas that reduce to TRUE/FALSE leaves. +- `modus_ponens`: proof-chain admission and refusal examples. +- `acyclicity`: circular dependency refusal cases. +- `out_of_regime`: quantified or predicate input outside propositional logic. +- `budget`: scalable ROBDD blowup cases that must refuse when over budget. + +## Interface Assumptions + +- Formula grammar: ADR-0202 section 1. +- Atom declaration and FeatureBundle binding: ADR-0202 section 2. +- TRUE/FALSE leaf identity: `T` / `F`. +- Budget refusal reason: `canonicalization_budget_exceeded`. +- Proof-chain rule and DAG fields are fixture data only until `proof_chain` + lands. + +## Non-Goals + +- No runtime wiring. +- No second canonicalizer implementation. +- No CNF/DNF fallback expectations. +- No predicate-logic equivalence claim. +- No repo capability claim. diff --git a/tests/fixtures/proof_chain/propositional_cases.json b/tests/fixtures/proof_chain/propositional_cases.json new file mode 100644 index 00000000..6e00ce8d --- /dev/null +++ b/tests/fixtures/proof_chain/propositional_cases.json @@ -0,0 +1,737 @@ +{ + "status": "ready_to_wire_when_proof_chain_lands", + "contract": "docs/decisions/ADR-0202-proposition-representation-contract.md", + "canonicalizer_contract": "docs/decisions/ADR-0201-proposition-canonicalizer.md", + "not_wired_into_live_suite": true, + "contains_concrete_formula_strings": true, + "conformance_policy": { + "non_refusal_cases": "All formula strings use the ADR-0202 grammar; every referenced atom is declared; every atom has a gloss and either FeatureBundle features or binding null.", + "refusal_cases": "Refusal probes either conform structurally and expect a proof-chain refusal, or intentionally present rejected input outside the formula grammar with a typed refusal reason." + }, + "cases": [ + { + "id": "PC-EQ-001", + "category": "equivalent_key", + "slot": "conjunction_commutativity", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Equivalent Boolean functions must share ROBDD identity under the fixed variable ordering.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains & Q_ground_wet", + "formula_b": "Q_ground_wet & P_rains", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-002", + "category": "equivalent_key", + "slot": "disjunction_commutativity", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Operand order must not affect function identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains | Q_ground_wet", + "formula_b": "Q_ground_wet | P_rains", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-003", + "category": "equivalent_key", + "slot": "conjunction_associativity", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Tree shape must not leak into canonical identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + }, + "R_traffic_slow": { + "gloss": "traffic is slow", + "binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "(P_rains & Q_ground_wet) & R_traffic_slow", + "formula_b": "P_rains & (Q_ground_wet & R_traffic_slow)", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-004", + "category": "equivalent_key", + "slot": "double_negation", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Logical involution must collapse to the original function.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "~~P_rains", + "formula_b": "P_rains", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-005", + "category": "equivalent_key", + "slot": "implication_expansion", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Implication and its propositional expansion must be the same function.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains -> Q_ground_wet", + "formula_b": "~P_rains | Q_ground_wet", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-006", + "category": "equivalent_key", + "slot": "de_morgan_conjunction", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Negated conjunction and disjunction of negations must share identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "~(P_rains & Q_ground_wet)", + "formula_b": "~P_rains | ~Q_ground_wet", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-007", + "category": "equivalent_key", + "slot": "conjunction_distributes_over_disjunction", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Equivalent functions with different syntactic expansion must canonicalize together.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + }, + "R_traffic_slow": { + "gloss": "traffic is slow", + "binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains & (Q_ground_wet | R_traffic_slow)", + "formula_b": "(P_rains & Q_ground_wet) | (P_rains & R_traffic_slow)", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-008", + "category": "equivalent_key", + "slot": "disjunction_idempotence", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Duplicate operands must not create distinct Boolean identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains | P_rains", + "formula_b": "P_rains", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-EQ-009", + "category": "equivalent_key", + "slot": "absorption", + "expected": "provable", + "expected_behavior": "identical_canonical_key", + "rationale": "Absorption catches syntactic normalizers that do not compute function identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains | (P_rains & Q_ground_wet)", + "formula_b": "P_rains", + "expected_relation": "same" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-NEQ-001", + "category": "different_key", + "slot": "implication_versus_converse_implication", + "expected": "not_provable", + "expected_behavior": "different_canonical_key", + "rationale": "Near-symmetric implications are not equivalent in general.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains -> Q_ground_wet", + "formula_b": "Q_ground_wet -> P_rains", + "expected_relation": "different" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-NEQ-002", + "category": "different_key", + "slot": "conjunction_versus_disjunction", + "expected": "not_provable", + "expected_behavior": "different_canonical_key", + "rationale": "The canonicalizer must not over-collapse common atoms.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains & Q_ground_wet", + "formula_b": "P_rains | Q_ground_wet", + "expected_relation": "different" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-NEQ-003", + "category": "different_key", + "slot": "grounded_atom_versus_negated_grounded_atom", + "expected": "not_provable", + "expected_behavior": "different_canonical_key", + "rationale": "Negation must change identity except for degenerate constants.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains", + "formula_b": "~P_rains", + "expected_relation": "different" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-NEQ-004", + "category": "different_key", + "slot": "strengthened_conjunction_versus_original_grounded_atom", + "expected": "not_provable", + "expected_behavior": "different_canonical_key", + "rationale": "Adding a premise changes the represented function.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "assertion": { + "kind": "canonical_key_relation", + "formula_a": "P_rains & Q_ground_wet", + "formula_b": "P_rains", + "expected_relation": "different" + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-TC-001", + "category": "tautology_or_contradiction", + "slot": "excluded_middle", + "expected": "provable", + "expected_behavior": "canonical_true_leaf", + "rationale": "A tautology must reduce to the TRUE terminal identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + } + }, + "assertion": { + "kind": "terminal_key", + "formula": "P_rains | ~P_rains", + "expected_canonical_key": "T", + "expected_is_tautology": true, + "expected_is_contradiction": false + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-TC-002", + "category": "tautology_or_contradiction", + "slot": "contradiction", + "expected": "not_provable", + "expected_behavior": "canonical_false_leaf", + "rationale": "A contradiction must reduce to the FALSE terminal identity.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + } + }, + "assertion": { + "kind": "terminal_key", + "formula": "P_rains & ~P_rains", + "expected_canonical_key": "F", + "expected_is_tautology": false, + "expected_is_contradiction": true + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-MP-001", + "category": "modus_ponens", + "slot": "valid_modus_ponens", + "expected": "provable", + "expected_behavior": "admit", + "rationale": "The first proof-chain rule should admit the canonical modus ponens form.", + "validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "premises": ["P_rains -> Q_ground_wet", "P_rains"], + "conclusion": "Q_ground_wet", + "rule": "modus_ponens", + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-MP-002", + "category": "modus_ponens", + "slot": "invalid_modus_ponens_wrong_conclusion", + "expected": "refused", + "expected_behavior": "refuse", + "expected_refusal_reason": "conclusion_mismatch", + "validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205", + "rule_reason_status": "pending phase 2.3 / ADR-0205", + "rationale": "The rule must refuse a conclusion not entailed by the dependencies.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + }, + "R_traffic_slow": { + "gloss": "traffic is slow", + "binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } } + } + }, + "premises": ["P_rains -> Q_ground_wet", "P_rains"], + "conclusion": "R_traffic_slow", + "rule": "modus_ponens", + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-MP-003", + "category": "modus_ponens", + "slot": "invalid_modus_ponens_missing_implication_premise", + "expected": "refused", + "expected_behavior": "refuse", + "expected_refusal_reason": "missing_implication", + "validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205", + "rule_reason_status": "pending phase 2.3 / ADR-0205", + "rationale": "The rule must refuse when the implication premise is missing.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "premises": ["P_rains"], + "conclusion": "Q_ground_wet", + "rule": "modus_ponens", + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-CYCLE-001", + "category": "acyclicity", + "slot": "two_node_dependency_cycle", + "expected": "refused", + "expected_behavior": "refuse", + "expected_refusal_reason": "circular_dependency", + "rationale": "Proof support must be a DAG; circular reasoning cannot prove the conclusion.", + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + } + }, + "proof_nodes": [ + { "id": "n1", "formula": "P_rains", "depends_on": ["n2"] }, + { "id": "n2", "formula": "Q_ground_wet", "depends_on": ["n1"] } + ], + "conclusion_node": "n1", + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + }, + { + "id": "PC-OOR-001", + "category": "out_of_regime", + "slot": "universally_quantified_predicate_statement", + "expected": "refused", + "expected_behavior": "refuse", + "expected_refusal_reason": "out_of_decidable_regime", + "rationale": "The propositional canonicalizer must not silently handle predicate logic.", + "atoms": {}, + "rejected_input": "forall x. rains(x) -> wet(x)", + "main_output_verified": { + "exception": "LogicRegimeError", + "reason": "out_of_decidable_regime" + }, + "conformance_checklist": { + "formula_grammar": false, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": false, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true, + "intentional_refusal_probe": true + } + }, + { + "id": "PC-OOR-002", + "category": "out_of_regime", + "slot": "existentially_quantified_predicate_statement", + "expected": "refused", + "expected_behavior": "refuse", + "expected_refusal_reason": "out_of_decidable_regime", + "rationale": "Quantification is outside the propositional equivalence corridor.", + "atoms": {}, + "rejected_input": "exists x. wet(x)", + "main_output_verified": { + "exception": "LogicRegimeError", + "reason": "out_of_decidable_regime" + }, + "conformance_checklist": { + "formula_grammar": false, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": false, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true, + "intentional_refusal_probe": true + } + }, + { + "id": "PC-BUDGET-001", + "category": "budget", + "slot": "scalable_robdd_pressure_family", + "expected": "refused", + "expected_behavior": "refuse_when_budget_exceeded", + "expected_refusal_reason": "canonicalization_budget_exceeded", + "rationale": "Large construction should refuse deterministically rather than churn or guess.", + "atoms": { + "X_b00": { "gloss": "schematic budget atom 00", "binding": null }, + "X_b01": { "gloss": "schematic budget atom 01", "binding": null }, + "X_b02": { "gloss": "schematic budget atom 02", "binding": null }, + "X_b03": { "gloss": "schematic budget atom 03", "binding": null }, + "X_b04": { "gloss": "schematic budget atom 04", "binding": null }, + "X_b05": { "gloss": "schematic budget atom 05", "binding": null }, + "X_b06": { "gloss": "schematic budget atom 06", "binding": null }, + "X_b07": { "gloss": "schematic budget atom 07", "binding": null } + }, + "assertion": { + "kind": "budget_refusal", + "formula": "X_b00 iff X_b01 iff X_b02 iff X_b03 iff X_b04 iff X_b05 iff X_b06 iff X_b07", + "max_nodes": 8 + }, + "conformance_checklist": { + "formula_grammar": true, + "all_formula_atoms_declared": true, + "atom_ids_stable_and_valid": true, + "all_atoms_have_gloss": true, + "bindings_are_features_or_null": true, + "no_quantifiers_predicates_or_functions": true, + "expected_outcome_allowed": true, + "equivalence_uses_canonical_key": true + } + } + ] +}