CodingThrust
diff --git a/‎.claude/skills/auto-pipeline/SKILL.md‎
Lines changed: 389 additions & 0 deletions b/‎.claude/skills/auto-pipeline/SKILL.md‎
Lines changed: 389 additions & 0 deletions
diff --git a/‎.claude/skills/check-issue/SKILL.md‎
Lines changed: 84 additions & 3 deletions b/‎.claude/skills/check-issue/SKILL.md‎
Lines changed: 84 additions & 3 deletions
diff --git a/‎.config/nextest.toml‎
Lines changed: 21 additions & 0 deletions b/‎.config/nextest.toml‎
Lines changed: 21 additions & 0 deletions
diff --git a/‎.github/workflows/ci.yml‎
Lines changed: 60 additions & 16 deletions b/‎.github/workflows/ci.yml‎
Lines changed: 60 additions & 16 deletions
@@ -199,6 +199,82 @@ If the algorithm is a high-level sketch rather than an implementable procedure
 
 ---
 
+## Rule Check 5: Completeness (fail label: `Incomplete`)
+
+**Goal:** Does the proposed mapping work for *every* instance of the source problem, not just the canonical case in the example?
+
+A reduction that only handles a subset of source instances (e.g., "assumes connected graph", "assumes no duplicate elements", "works only when k is even") is **not a valid polynomial-time reduction** unless the issue explicitly:
+- restricts the source to a sub-variant that the codebase actually exposes as a distinct model, AND
+- the restriction is part of the algorithm statement, not a hidden assumption.
+
+This check is **mandatory** for every `[Rule]` issue and must be backed by **explicit literature and codebase research** — not vibes.
+
+### 5a: Literature research (mandatory)
+
+For the cited construction(s):
+
+1. Find the original paper or textbook section that defines the reduction.
+2. Read the **statement of the theorem**: what does it claim the reduction handles? Look for phrases like:
+   - "for any instance of P" → covers all instances (good)
+   - "for a P-instance such that ..." → has a precondition (must be flagged)
+   - "in the special case where ..." → only a special case (must be flagged)
+3. Read the **proof**: are there steps that silently assume something about the source (no isolated vertices, no zero weights, integer-valued capacities, ...)?
+
+Use the same fallback chain as Check 3c.
+
+If the cited paper is **not actually a reduction from the full source problem** but from a restricted variant → **Fail** with the precise restriction quoted from the paper. The fix is one of: (a) add a preprocessing step that reduces the full source to the restricted variant, (b) split into a `[Rule]` issue from the actual restricted source, or (c) drop the reduction.
+
+### 5b: Codebase corner-case research (mandatory)
+
+Check the actual codebase to see what shape the source problem can take:
+
+```bash
+pred show <Source> --json
+```
+
+Read the `size_fields` and any variant getters, then enumerate corner cases the issue's algorithm must handle:
+
+| Class | Example corner cases the reduction must accept |
+|---|---|
+| Graph-input problems | empty graph, single vertex, isolated vertices, self-loops if the model allows them, parallel edges if allowed, disconnected components, complete graph |
+| Weighted problems | all weights equal, all weights zero, mixed signs (if the weight type allows), one weight dominating the rest |
+| Formula/circuit | empty clause set, single-literal clauses, tautological clauses, repeated variables in a clause |
+| Set systems | empty universe, empty subsets, identical subsets, universe element appearing in no subset |
+| Algebraic | zero matrix, identity, singular matrix |
+
+Then trace the **issue's** algorithm by hand against at least 2 corner cases that are not the worked example:
+
+1. Pick a corner case from the table above that the source model actually allows.
+2. Simulate the issue's construction step by step.
+3. Check: is the target problem well-defined? Does solution extraction still work?
+
+Also grep the codebase for any existing rule whose source has the same problem name — if it already handles certain corner cases, the new rule should at least match that coverage:
+
+```bash
+grep -rl "impl.*ReduceTo.*for <Source>" src/rules/
+```
+
+Read 1–2 of those existing rules for how they handle edge inputs.
+
+If the issue's algorithm **crashes, produces an invalid target instance, or loses information** on a legitimate corner case → **Fail** with the corner case spelled out.
+
+If the issue's algorithm appears to handle corner cases correctly but the issue body doesn't *state* this explicitly → **Warn** ("works on tested corner cases, but the algorithm description does not address edge inputs — please document").
+
+### 5c: Verdict
+
+| Finding | Verdict |
+|---|---|
+| Literature explicitly covers all instances AND traced corner cases work | **Pass** |
+| Literature explicitly covers all instances but issue is silent on corner cases | **Warn** |
+| Literature has a precondition the issue ignores | **Fail** |
+| Traced corner case breaks the algorithm | **Fail** |
+
+(If the cited reference doesn't actually contain the reduction at all, Check 3c already catches it — don't double-flag here.)
+
+Report the literature evidence and the corner cases you traced in the comment — this is the most expensive check and reviewers will want to see your work.
+
+---
+
 # Part B: Model Issue Checks
 
 Applies when the title contains `[Model]`.
@@ -359,9 +435,10 @@ Post a single GitHub comment. The table adapts to the issue type:
 | Usefulness | ✅ Pass | No existing direct reduction Source → Target |
 | Non-trivial | ✅ Pass | Gadget construction with penalty terms |
 | Correctness | ❌ Fail | Paper "Smith 2020" not found on arxiv or Semantic Scholar |
+| Completeness | ⚠️ Warn | Algorithm correct on traced corner cases but issue body silent on edge inputs |
 | Well-written | ⚠️ Warn | Symbol `m` used in overhead table but not defined in algorithm |
 
-**Overall: 2 passed, 1 failed, 1 warning**
+**Overall: 2 passed, 1 failed, 2 warnings**
 
 ---
 
@@ -374,6 +451,9 @@ Post a single GitHub comment. The table adapts to the issue type:
 ### Correctness
 [Per-reference verification results, any better algorithms found]
 
+### Completeness
+[Literature passages cited (with quote + section/theorem number) showing whether the construction covers all source instances, and the corner cases you traced by hand with the algorithm — including any that broke or any preconditions you discovered]
+
 ### Well-written
 [Specific items to fix]
 
@@ -423,13 +503,14 @@ gh issue edit <NUMBER> --add-label "Useless"     # if Check 1 failed
 gh issue edit <NUMBER> --add-label "Trivial"      # if Check 2 failed
 gh issue edit <NUMBER> --add-label "Wrong"        # if Check 3 failed
 gh issue edit <NUMBER> --add-label "PoorWritten"  # if Check 4 failed
+gh issue edit <NUMBER> --add-label "Incomplete"   # if Rule Check 5 failed
 
-# "Good" label requires: zero failures AND zero warnings on Usefulness or Correctness.
+# "Good" label requires: zero failures AND zero warnings on Usefulness, Correctness, or Completeness.
 # Warnings on Non-trivial or Well-written alone do NOT block "Good".
 gh issue edit <NUMBER> --add-label "Good"
 
 # If re-checking after fixes, remove stale failure labels and add "Good" if now passing
-gh issue edit <NUMBER> --remove-label "Useless,Trivial,Wrong,PoorWritten" 2>/dev/null
+gh issue edit <NUMBER> --remove-label "Useless,Trivial,Wrong,PoorWritten,Incomplete" 2>/dev/null
 gh issue edit <NUMBER> --add-label "Good"
 ```
 
 
@@ -0,0 +1,21 @@
+# nextest configuration.
+#
+# Project policy is that no single test exceeds 5s (see .claude/CLAUDE.md).
+# slow-timeout is a CI safety net far above that budget: a test is flagged slow
+# every 60s and forcibly terminated after 5 periods (300s). This bounds a truly
+# hung test (cf. issue #1069, where big_o expansion looped indefinitely and the
+# whole job was SIGTERM-killed at the runner level) — nextest reports it as a
+# clean per-test timeout failure instead of stalling the job.
+#
+# The large headroom (300s, not a tight ~10s) is deliberate. The subprocess
+# example tests in tests/suites/examples.rs shell out to `cargo run --example
+# … --features ilp-highs`:
+#   - In the Test job, CI pre-builds those examples (see ci.yml) so the
+#     subprocess reuses artifacts and each test runs in well under a second.
+#   - In the Code Coverage job, the subprocess inherits llvm-cov's
+#     `-C instrument-coverage` RUSTFLAGS, so it recompiles the examples
+#     *instrumented* (a non-instrumented pre-build would not match its
+#     fingerprint, so pre-building there is pointless). That instrumented
+#     recompile legitimately takes >120s, hence the 300s bound.
+[profile.default]
+slow-timeout = { period = "60s", terminate-after = 5 }
@@ -6,62 +6,106 @@ on:
   pull_request:
     branches: [ main, develop ]
 
+# Cancel superseded runs on the same ref (e.g. rapid pushes to a PR).
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+# Least privilege: jobs only read the repo; codecov auth is via token secret.
+permissions:
+  contents: read
+
 env:
   CARGO_TERM_COLOR: always
   RUST_BACKTRACE: 1
+  # Incremental compilation hurts cold CI builds and bloats the cache; disable it
+  # (recommended by Swatinem/rust-cache).
+  CARGO_INCREMENTAL: 0
+  # Tolerate transient registry/network blips.
+  CARGO_NET_RETRY: 10
+  RUSTUP_MAX_RETRIES: 10
 
 jobs:
-  # Run clippy
+  # Formatting — cheap, fails fast, no build/cache needed.
+  fmt:
+    name: Rustfmt
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: rustfmt
+      - name: Check formatting
+        run: cargo fmt --all --check
+
+  # Lints.
   clippy:
     name: Clippy
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@stable
         with:
           components: clippy
       - uses: Swatinem/rust-cache@v2
       - name: Run clippy
         run: cargo clippy --all-targets --features ilp-highs -- -D warnings
 
-  # Build and test
+  # Build, test (nextest), doc tests, and paper.
   test:
     name: Test
     runs-on: ubuntu-latest
+    # Single feature set across compile + test + doctest so artifacts are reused
+    # (no redundant full recompile between steps).
+    env:
+      FEATURES: "ilp-highs example-db"
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@stable
+      - uses: taiki-e/install-action@v2
+        with:
+          tool: nextest
       - uses: Swatinem/rust-cache@v2
+      - name: Install typst
+        uses: typst-community/setup-typst@v5
+
+      - name: Compile tests
+        run: cargo nextest run --no-run --workspace --features "$FEATURES"
 
-      - name: Build
-        run: cargo build --features ilp-highs --verbose
+      # The subprocess example tests (tests/suites/examples.rs) shell out to
+      # `cargo run --example … --features ilp-highs`. Pre-build those example
+      # binaries with that exact feature set so the subprocess reuses artifacts
+      # instead of recompiling the whole crate mid-test (which otherwise adds
+      # 60s+ to a single test's wall-clock and would trip the nextest timeout).
+      - name: Build examples (for subprocess tests)
+        run: cargo build --examples --features ilp-highs
 
       - name: Run tests
-        run: cargo test --features "ilp-highs example-db" --workspace --verbose
+        run: cargo nextest run --workspace --features "$FEATURES"
 
+      # nextest does not run doc tests; run them separately (reuses the build).
       - name: Run doc tests
-        run: cargo test --doc --features ilp-highs --verbose
-
-      - name: Install typst
-        uses: typst-community/setup-typst@v4
+        run: cargo test --doc --features "$FEATURES" --verbose
 
       - name: Build paper
         run: make paper
 
-  # Code coverage
+  # Coverage. Feature set intentionally matches the historical coverage gate
+  # (ilp-highs only) to keep the codecov baseline stable.
   coverage:
     name: Code Coverage
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@stable
         with:
           components: llvm-tools-preview
+      - uses: taiki-e/install-action@v2
+        with:
+          tool: cargo-llvm-cov,nextest
       - uses: Swatinem/rust-cache@v2
-      - name: Install cargo-llvm-cov
-        uses: taiki-e/install-action@cargo-llvm-cov
       - name: Generate coverage
-        run: cargo llvm-cov --features ilp-highs --workspace --lcov --output-path lcov.info
+        run: cargo llvm-cov nextest --features ilp-highs --workspace --lcov --output-path lcov.info
       - name: Upload to codecov.io
         uses: codecov/codecov-action@v5
         with: