Symbolic growth, exact Pareto path search, and deterministic solver backends

.claude/CLAUDE.md

@@ -25,7 +25,7 @@ These repo-local skills live under `.claude/skills/*/SKILL.md`.
 - [review-quality](skills/review-quality/SKILL.md) -- Generic code quality review: DRY, KISS, cohesion/coupling, test quality, HCI. Read-only, no code changes. Called by `review-pipeline`.
 - [fix-pr](skills/fix-pr/SKILL.md) -- Resolve PR review comments, fix CI failures, and address codecov coverage gaps. Uses `gh api` for codecov (not local `cargo-llvm-cov`).
 - [write-model-in-paper](skills/write-model-in-paper/SKILL.md) -- Write or improve a problem-def entry in the Typst paper (standalone, for improving existing entries). Core instructions are inlined in `add-model` Step 6.
-- [write-rule-in-paper](skills/write-rule-in-paper/SKILL.md) -- Write or improve a reduction-rule entry in the Typst paper (standalone, for improving existing entries). Core instructions are inlined in `add-rule` Step 5.
+- [write-rule-in-paper](skills/write-rule-in-paper/SKILL.md) -- Write or improve a reduction-rule entry in the Typst paper (standalone, for improving existing entries). Core instructions are inlined in `add-rule` Step 6.
 - [release](skills/release/SKILL.md) -- Create a new crate release. Determines version bump from diff, verifies tests/clippy, then runs `make release`.
 - [check-issue](skills/check-issue/SKILL.md) -- Quality gate for `[Rule]` and `[Model]` issues. Checks usefulness, non-triviality, correctness of literature, and writing quality. Posts structured report and adds failure labels.
 - [fix-issue](skills/fix-issue/SKILL.md) -- Fix quality issues found by check-issue — auto-fixes mechanical problems, brainstorms substantive issues with human, then re-checks and moves to Ready.
@@ -59,7 +59,7 @@ make fmt-check      # Check code formatting
 make clippy         # Run clippy lints
 make doc            # Build mdBook documentation (includes reduction graph export)
 make mdbook         # Build and serve mdBook with live reload
-make paper          # Build Typst paper from checked-in example fixtures
+make paper          # Generate example data and build the Typst paper
 make coverage       # Generate coverage report (>95% required)
 make check          # Quick pre-commit check (fmt + clippy + test)
 make rust-export    # Generate Julia parity test data (mapping stages)
@@ -158,6 +158,8 @@ Max<V>, Min<V>, Sum<W>, Or, And, Extremum<V>, ExtremumSense
 - `Solver::solve()` computes the aggregate value for any `Problem` whose `Value` implements `Aggregate`
 - `BruteForce::find_witness()` / `find_all_witnesses()` recover witnesses only when `P::Value::supports_witnesses()`
 - `ReductionResult` provides `target_problem()` and `extract_solution()` for witness/config workflows; `AggregateReductionResult` provides `extract_value()` for aggregate/value workflows
+- Every direct `extract_solution()` must call `validate_target_solution()` once before decoding; composed extractors delegate validation to the first direct decoder.
+- Decode only the reduction's defined mathematical mapping. Reject malformed structure with `ExtractionError`; never panic, truncate, clamp, invent defaults, or add recovery branches. Explicit mathematical alternatives and sentinels are allowed. Test successful decoding and every rejected representation.
 - CLI-facing dynamic formatting uses aggregate wrapper names directly (for example `Max(2)`, `Min(None)`, `Or(true)`, or `Sum(56)`)
 - Graph types: SimpleGraph, PlanarGraph, BipartiteGraph, UnitDiskGraph, KingsSubgraph, TriangularSubgraph
 - Weight types: `One` (unit weight marker), `i32`, `f64` — all implement `WeightElement` trait
@@ -208,14 +210,14 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 - Aggregate-only models are first-class in `declare_variants!`; aggregate-only and Turing reduction edges still need manual `ReductionEntry` wiring because `#[reduction]` only registers witness/config reductions today
 - Exact registry dispatch lives in `src/registry/`; alias resolution and partial/default variant resolution live in `problemreductions-cli/src/problem_name.rs`
 - `pred create` schema-driven dispatch lives in `problemreductions-cli/src/commands/create.rs` (`create_schema_driven()`)
-- Canonical paper and CLI examples live in `src/example_db/model_builders.rs` and `src/example_db/rule_builders.rs`
+- Canonical model examples live in `src/example_db/model_builders.rs`; rule examples live beside their rules and are collected by `src/rules/mod.rs`
 
 ## Conventions
 
 ### File Naming
 - Reduction files: `src/rules/<source>_<target>.rs` (e.g., `maximumindependentset_qubo.rs`)
 - Model files: `src/models/<category>/<name>.rs` — category is by input structure: `graph/` (graph input), `formula/` (boolean formula/circuit), `set/` (universe + subsets), `algebraic/` (matrix/linear system/lattice), `misc/` (other)
-- Canonical examples: builder functions in `src/example_db/rule_builders.rs` and `src/example_db/model_builders.rs`
+- Canonical examples: model builders in `src/example_db/model_builders.rs`; rule-local `canonical_rule_example_specs()` functions collected by `src/rules/mod.rs`
 - Example binaries in `examples/`: utility/export tools and pedagogical demos only (not per-reduction files)
 - Test naming: `test_<source>_to_<target>_closed_loop`
 
@@ -261,7 +263,7 @@ Model review automation checks for a dedicated test file under `src/unit_tests/m
 - `.claude/` — Claude Code instructions and skills
 - `docs/book/` — mdBook user documentation (built with `make doc`)
 - `docs/paper/reductions.typ` — Typst paper with problem definitions and reduction theorems
-- `src/example_db/` — Canonical model/rule examples: `model_builders.rs`, `rule_builders.rs` (in-memory builders), `specs.rs` (per-module invariant specs), consumed by `pred create --example` and paper exports
+- `src/example_db/` — Model builders, shared example specs, and rule-example aggregation consumed by `pred create --example` and paper exports
 - `examples/` — Export utilities, graph-analysis helpers, and pedagogical demos
 
 ## Documentation Requirements

.claude/skills/add-rule/SKILL.md

@@ -106,13 +106,19 @@ impl ReductionResult for ReductionXToY {
     type Source = SourceType;
     type Target = TargetType;
     fn target_problem(&self) -> &Self::Target { &self.target }
-    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
-        // Map target solution back to source solution
-        // If Step 1 ran: translate the verified Python extract_solution() logic
+    fn extract_solution(
+        &self,
+        target_solution: &[usize],
+    ) -> crate::rules::ExtractionResult<Vec<usize>> {
+        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
+        let source_solution = /* translate the verified mathematical mapping exactly */;
+        Ok(source_solution)
     }
 }
 ```
 
+Every direct extractor must call `validate_target_solution()` once before decoding. It checks only length and value domains, not feasibility, optimality, or rule-specific structure; reject malformed structure with `ExtractionError`.
+
 **ReduceTo with `#[reduction]` macro** (overhead is **required**):
 ```rust
 #[reduction(overhead = {
@@ -156,16 +162,18 @@ Additional recommended tests:
 - Edge cases (empty graph, single vertex, etc.)
 - Weight preservation (if applicable)
 
+Test every malformed representation distinguished by the decoder (for example, zero or multiple one-hot selections, or duplicate permutation entries). The canonical example supplies shared wrong-length and out-of-domain tests.
+
 For aggregate-only reductions, replace the closed-loop witness test with value-chain tests:
 - Solve the target with `Solver::solve()`
 - Map the aggregate value back with `extract_value()`
 - If testing a path, use `ReductionGraph::reduce_aggregate_along_path(...)`
 
 Link via `#[cfg(test)] #[path = "..."] mod tests;` at the bottom of the rule file.
 
-## Step 5: Add canonical example to example_db
+## Step 5: Add canonical example
 
-Add a builder function in `src/example_db/rule_builders.rs` that constructs a small, canonical instance for this reduction. Follow the existing patterns in that file. Register the builder in `build_rule_examples()`.
+Define `canonical_rule_example_specs()` in the rule module and include it from `src/rules/mod.rs::canonical_rule_example_specs()`. This enrolls the rule in shared round-trip, wrong-length, and out-of-domain extraction tests.
 
 ## Step 6: Document in paper (MANDATORY — DO NOT SKIP)
 
@@ -231,11 +239,11 @@ Checklist: notation self-contained, complexity cited, overhead consistent, examp
 ```bash
 cargo run --example export_graph    # Generate reduction_graph.json for docs/paper builds
 cargo run --example export_schemas  # Generate problem schemas for docs/paper builds
-make regenerate-fixtures            # Regenerate example_db/fixtures/examples.json (slow, needs ILP)
+cargo run --features "example-db" --example export_examples
 make test clippy                    # Must pass
 ```
 
-`make regenerate-fixtures` is required so the paper can load the new rule's example data from `src/example_db/fixtures/examples.json`. Without it, the `reduction-rule` entry in Step 6 will reference missing fixture data.
+`export_examples` refreshes the gitignored `docs/paper/data/examples.json` used by the paper.
 
 Structural and quality review is handled by the `review-pipeline` stage, not here. The run stage just needs to produce working code.
 
@@ -251,6 +259,8 @@ Structural and quality review is handled by the `review-pipeline` stage, not her
 
 Adding a witness-preserving reduction rule does NOT require CLI changes -- the reduction graph is auto-generated from `#[reduction]` macros and the CLI discovers paths dynamically. However, both source and target models must already be fully registered through their model files (`declare_variants!`), aliases as needed in `problem_name.rs`, and `pred create` support where applicable (see `add-model` skill).
 
+`ExtractionError` already propagates through `pred extract` and bundle `pred solve`; add a rule-specific CLI test only when the CLI surface changes.
+
 Aggregate-only reductions currently have a narrower CLI surface:
 - `pred solve <problem.json>` can still compute direct aggregate values for aggregate-only problems
 - `pred reduce` and `pred solve bundle.json` remain witness-only workflows and reject aggregate-only paths
@@ -261,7 +271,7 @@ Aggregate-only reductions currently have a narrower CLI surface:
 - Rule file: `src/rules/<sourcelower>_<targetlower>.rs` -- no underscores within a problem name
   - e.g., `maximumindependentset_qubo.rs`, `minimumvertexcover_maximumindependentset.rs`
 - Test file: `src/unit_tests/rules/<sourcelower>_<targetlower>.rs`
-- Canonical example: builder function in `src/example_db/rule_builders.rs`
+- Canonical example: `canonical_rule_example_specs()` in the rule module, included from `src/rules/mod.rs`
 
 ## Common Mistakes
 
@@ -272,9 +282,10 @@ Aggregate-only reductions currently have a narrower CLI surface:
 | Wrong overhead expression | Must accurately reflect the size relationship |
 | Adding extra reduction metadata or duplicate primitive endpoint registration | Keep one primitive registration per endpoint pair and use only the `overhead` form of `#[reduction]` |
 | Missing `extract_solution` mapping state | Store any index maps needed in the ReductionResult struct |
-| Not adding canonical example to `example_db` | Add builder in `src/example_db/rule_builders.rs` |
+| Permissive extraction | Validate first, then map exactly or return `ExtractionError` |
+| Not adding a canonical example | Add the rule-local spec and include it from `src/rules/mod.rs` |
 | Not regenerating reduction graph | Run `cargo run --example export_graph` after adding a rule |
-| Skipping Step 5 (paper documentation) | **Every rule MUST have a `reduction-rule` entry in the paper. This is mandatory, not optional. PRs without documentation will be rejected.** |
+| Skipping Step 6 (paper documentation) | **Every rule MUST have a `reduction-rule` entry in the paper. This is mandatory, not optional. PRs without documentation will be rejected.** |
 | Source/target model not fully registered | Both problems must already have `declare_variants!`, aliases as needed, and CLI create support -- use `add-model` skill first |
 | Treating a direct-to-ILP rule as a toy stub | Direct ILP reductions need exact overhead metadata and strong semantic regression tests, just like other production ILP rules |
 | Skipping verification for complex reductions | Verification is default for a reason — `--no-verify` is for trivial identity/complement reductions only |

.claude/skills/final-review/SKILL.md

@@ -168,12 +168,12 @@ Use `AskUserQuestion` with your recommendation:
 
 Scan the PR diff for dangerous actions:
 
-- **Blacklisted files**: If the diff touches `docs/src/reductions/reduction_graph.json`, `docs/src/reductions/problem_schemas.json`, or `src/example_db/fixtures/examples.json` (legacy, no longer exists), **block merge**. These files are auto-generated and must not be committed in PRs — they are rebuilt by CI/`make doc`/`make paper`. Flag immediately and recommend OnHold.
+- **Blacklisted files**: If the diff touches `docs/src/reductions/reduction_graph.json` or `docs/src/reductions/problem_schemas.json`, **block merge**. These files are auto-generated and must not be committed in PRs — they are rebuilt by CI/`make doc`/`make paper`. Flag immediately and recommend OnHold.
 - **Removed features**: Any existing model, rule, test, or example deleted?
 - **Unrelated changes**: Files modified that don't belong to this PR (e.g., changes to unrelated models/rules, CI config, Cargo.toml dependency changes not needed for this PR)
 - **Force push indicators**: Any sign of history rewriting
 - **Broad modifications**: Changes to core traits, macros, or shared infrastructure that could affect other features
-- **No committed `examples.json`**: The example database is generated on demand by `make paper` (via `export_examples`). PRs should not commit `src/example_db/fixtures/examples.json` (legacy path, deleted) or `docs/paper/data/examples.json` (current output path) — both are gitignored build artifacts.
+- **No committed `examples.json`**: The example database is generated on demand by `make paper` (via `export_examples`). Do not commit the gitignored `docs/paper/data/examples.json` build artifact.
 
 Report findings with fix options for each concern:
 

.claude/skills/issue-to-pr/SKILL.md

@@ -92,12 +92,12 @@ Write implementation plan to `docs/plans/YYYY-MM-DD-<slug>.md` using `superpower
 The plan MUST reference the appropriate implementation skill and follow its steps:
 
 - **For ordinary `[Model]` issues:** Follow [add-model](../add-model/SKILL.md) Steps 1-7 as the action pipeline
-- **For `[Model]` issues that explicitly claim direct ILP solving:** Follow [add-model](../add-model/SKILL.md) Steps 1-7 **and** [add-rule](../add-rule/SKILL.md) Steps 1-6 for the direct `<Problem> -> ILP` rule in the same plan / PR
+- **For `[Model]` issues that explicitly claim direct ILP solving:** Follow [add-model](../add-model/SKILL.md) Steps 1-7 **and** [add-rule](../add-rule/SKILL.md) Steps 1-7 for the direct `<Problem> -> ILP` rule in the same plan / PR
 - **For `[Rule]` issues:** Follow [add-rule](../add-rule/SKILL.md) Steps 1-7 as the action pipeline. By default, `/add-rule` runs mathematical verification (Step 1) before implementation. If `--no-verify` was passed, include `--no-verify` when invoking `/add-rule` to skip verification.
 
 Include the concrete details from the issue (problem definition, reduction algorithm, example, etc.) mapped onto each step.
 
-**Plan batching:** The paper writing step (add-model Step 6 / add-rule Step 5) MUST be in a **separate batch** from the implementation steps, so it gets its own subagent with fresh context. It depends on the implementation being complete (needs exports). Example batch structure for a `[Model]` plan:
+**Plan batching:** The paper writing step (add-model Step 6 / add-rule Step 6) MUST be in a **separate batch** from the implementation steps, so it gets its own subagent with fresh context. It depends on the implementation being complete (needs exports). Example batch structure for a `[Model]` plan:
 - Batch 1: Steps 1-5.5 (implement model, register, CLI, tests)
 - Batch 2: Step 6 (write paper entry — depends on batch 1 for exports)
 
@@ -112,8 +112,8 @@ For a `[Model]` issue with an explicit direct ILP claim, use:
 - Otherwise, ensure the information provided is enough to implement a solver.
 
 **Example rules:**
-- Implement the user-provided example instance in the canonical `example_db` path for the issue (`src/example_db/model_builders.rs` or `src/example_db/rule_builders.rs`, as appropriate).
-- Run the relevant export and fixture regeneration steps; verify the generated example data against the user-provided information.
+- Implement the user-provided example in `src/example_db/model_builders.rs` for a model, or in the rule-local `canonical_rule_example_specs()` for a rule.
+- Run the relevant exports and verify the generated example data against the user-provided information.
 - Present in `docs/paper/reductions.typ` in tutorial style with clear intuition (see KColoring->QUBO section for reference).
 
 ### 6. Create PR (or Resume Existing)

.claude/skills/review-paper/SKILL.md

@@ -46,7 +46,7 @@ For each of the 10 entries, read the full entry text and evaluate against the ch
 | M3. Self-contained notation | Every symbol in `def` is defined before first use |
 | M4. Background text | Body contains at least 2 sentences of background/motivation |
 | M5. Example present | Body contains `*Example.*` or `Example.` |
-| M6. Example from fixture | Example data matches `src/example_db/fixtures/examples.json` (not invented) — check by loading the JSON and comparing |
+| M6. Example from fixture | Example data matches `docs/paper/data/examples.json` (not invented) — check by loading the JSON and comparing |
 | M7. Figure present | Body contains `#figure(` |
 | M8. Pred commands | Body contains `pred-commands(` or `pred create` |
 | M9. Algorithm citation | Complexity claims have `@citation` or a footnote explaining absence |
@@ -72,7 +72,7 @@ For each of the 10 entries, read the full entry text and evaluate against the ch
 | M3. Proof length | Proof is at least 3 sentences (not just "trivial" or a one-liner) |
 | M4. Overhead documented | Overhead is auto-generated from JSON (verify edge exists in `reduction_graph.json`) |
 | M5. Example present | `example: true` and example renders correctly |
-| M6. Example from fixture | Example data matches `src/example_db/fixtures/examples.json` |
+| M6. Example from fixture | Example data matches `docs/paper/data/examples.json` |
 | M7. Pred commands | Example section contains `pred-commands(` with create/reduce/evaluate pipeline |
 | M8. Both directions | If the reverse rule also exists in the graph, check it has its own entry |