fix: silent errors, unbounded searches, and two order-of-magnitude regressions - #294
Merged
Conversation
…gressions Pre-release hardening for 3.8, which will run unattended multi-day loops. Four of these were silent errors *shipped in 3.7* — confident wrong answers with no exception and no flag, the failure class that compounds in a research loop because the loop's own consistency checks confirm the poisoned result. Silent errors ------------- `decide` proved false theorems and returned certificates that fail their own equation. `forall x. (3x+2)^2 > 0` returned True — it is false at x = -2/3 — and `exists x. 3x-2 = 0` returned witness 1/2, for which 3x-2 = -1/2. Wrong exactly when the deciding point had a non-dyadic denominator, because `RootInterval` documents that an exact rational root is reported as lo == hi and `real_roots` did not deliver it, so CAD's all-dyadic sample set never tested the root. Both corpus cases that existed were dyadic, which is why it survived. 18 wrong verdicts in the first 150 random polynomials before, 0 in 1000 after. The same completeness gap in the two-variable path escalated only on Eq/Ne: 90 wrong of 243 before, 0 after, with no correct answers lost to refusal. `Matrix.nullspace()` returned a basis whose vectors are not in the kernel, for any 2x2 with a symbolic determinant. `[[x,0],[0,1]]` gave rank 2 *and* nullity 1 -- 2 + 1 = 3 for a two-column matrix -- because the full-rank gate recognised only a literal non-zero constant, so every non-literal determinant fell into the rank-1 branch. "Could not prove det != 0" read as "det = 0", the mirror of the rref defect. The gate is now three-valued; the eigen paths state `KnownSingular::Yes` instead, since det(A - lambda I) = 0 holds by construction. `simplify(0 * 0^-1)` returned 1 -- a value the expression cannot take -- and it was four independent rules, not one, including an egglog ruleset that unions 0 and 1 into a single e-class, which no rewrite can patch because an e-graph cannot carry the side condition. Reachable as `diff(2/(x-x), x)`. Unbounded and uninterruptible searches -------------------------------------- `limit(sqrt(x^2+x) - x, x, +inf)` never returned; it now answers 1/2 in about a millisecond. Budget checkpoints now sit on the paths that were actually hot (measured, not guessed -- it was never Gruntz), so wall_ms binds to ~1.1x instead of 7-12x or never, and `request_cancel` reaches a running engine because `integrate` and `limit` release the GIL. `batch_map(parallel=True)` ignored budgets entirely and reported the timeout as E-INT-001 -- a mathematical verdict a loop records as a closed branch -- and now propagates an absolute deadline so N items cannot each get a fresh wall_ms. `run_with_wall_fallback` poisoned the whole process: one expired candidate left the sticky cancel flag set and every later call failed with E-BUDGET-003 forever. Performance ----------- `Matrix::det` documented Bareiss and implemented O(n!) cofactor expansion: 9x9 integers 1408 ms -> 0.09 ms, measured exponent n^13.4 -> n^3.13, from 400x slower than SymPy to 28x faster. `poly_gcd` over Q[x] now calls FLINT: degree 128, 272882 ms -> 0.40 ms. And the Risch rational route spent minutes inside `kpoly_gcd` computing a RootSum that `verify_antiderivative` is structurally guaranteed to reject, so the two verify-gated routes now decline up front: 869 s -> 154 ms on one integrand, 106 s -> 11.5 ms on another. Docs ---- `decide` was documented as *complete*, as a selling point, in two places. The Sphinx matrix page documented `Matrix.inv()` (the method is `inverse()`) and `M[i, j]` subscripting (raises TypeError). `TESTING.md`'s valgrind loop globbed a package name that matches zero binaries and passed while checking nothing, and claimed UBSan coverage that does not exist. `alkahest_core::` throughout the docs is a workspace-local alias -- external crates need `alkahest_cas::`. The CHANGELOG now opens with which silent errors shipped in 3.7, so anyone with results from that version knows what to recheck. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
📝 WalkthroughWalkthroughThis PR hardens arithmetic, CAD, simplification, integration, symbolic linear algebra, expression-depth handling, Python bindings, workload control, and operational documentation. It adds refusal propagation, budget and cancellation handling, panic-safe validation, and expanded regression coverage. ChangesCore correctness and safety
Runtime controls and interfaces
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 13
Note
Due to the large number of review comments, Critical, Major severity comments were prioritized as inline comments.
🟡 Minor comments (13)
tests/silent_errors/corpus.py-159-171 (1)
159-171: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winRemove the unsupported
codekeyword fromak.CadError. Both the nativePyCadErrorand the Python fallback do not acceptcode; passing it raisesTypeError.str(X)is"x", so the witness lookup is valid.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/silent_errors/corpus.py` around lines 159 - 171, Update _witness_residual to raise ak.CadError without the unsupported code keyword when decide returns no witness, preserving the existing error message and residual calculation.alkahest-core/src/simplify/egraph.rs-303-320 (1)
303-320: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winClassify zero-valued
Rationalbases asQuick::Zero.
ExprPool::rational(0, 1)creates anExprData::Rationalnode. The current match classifies everyExprData::Rationalbase asQuick::NonZero, so a zero-valued rational with a negative exponent bypassesis_zero_denominator. Checkr.0 == 0and returnQuick::Zerofor that case.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/simplify/egraph.rs` around lines 303 - 320, Update the ExprData::Rational branch in the quick classification match to inspect the rational numerator and return Quick::Zero when r.0 == 0; keep nonzero rationals classified as Quick::NonZero so negative-exponent handling reaches is_zero_denominator correctly.docs/mdbook/src/smt.md-96-97 (1)
96-97: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winQualify the witness guarantee.
Line [96] says
decidereturns a verdict plus a verified witness. A true existential result can havewitness=Nonewhen no rational witness is available;CHANGELOG.mdLines [363]-[365] documents∃x. x² = 2 → (True, None). Say “when available” to prevent loops from treating a missing witness as a failure.This behavior is documented in
CHANGELOG.mdLines [363]-[365].🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/mdbook/src/smt.md` around lines 96 - 97, Update the SMT documentation statement about decide’s result to qualify that the verified witness is returned when available, while preserving the existing verdict description. Ensure the text does not imply that every true existential result includes a witness.docs/sphinx/api/autoresearch.rst-15-18 (1)
15-18: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winDescribe refusal codes as a set, not one code.
Lines [15]-[18] say each module has one refusal code. The same page lists
E-ANSATZ-004andE-LINALG-010at Lines [47]-[52].python/alkahest/crosscheck.pyalso documentsE-XCHECK-001for translation refusals. Change the note to say “examples include” or list all route-refusal codes. Otherwise, search loops may classify other refusals incorrectly.This comparison uses the refusal declarations in this file and
python/alkahest/crosscheck.py.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/sphinx/api/autoresearch.rst` around lines 15 - 18, Update the refusal-code note in the autoresearch documentation to describe the codes as a set of route-specific examples rather than claiming each module has exactly one code. Use wording such as “examples include” and ensure it does not imply that listed codes like E-ANSATZ-003, E-XCHECK-002, and E-SMT-003 are exhaustive.CONTRIBUTING.md-34-40 (1)
34-40: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winDocument the complete ASan environment.
The ASan CI step sets
LSAN_OPTIONS=detect_leaks=0, but the documented command does not. Add this variable to the command so users can reproduce the CI configuration.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@CONTRIBUTING.md` around lines 34 - 40, Update the documented ASan command in CONTRIBUTING.md to include LSAN_OPTIONS=detect_leaks=0 alongside RUSTFLAGS, preserving the existing cargo package, target, and build-std arguments so it matches the CI environment.docs/mdbook/src/simplification.md-146-146 (1)
146-146: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winState both language-specific paths.
Use
alkahest_cas::experimental::{simplify_par, simplify_redex}for Rust andalkahest.simplify_par/alkahest.simplify_redexfor Python. These Python functions are not inalkahest.experimental.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/mdbook/src/simplification.md` at line 146, Update the documentation sentence in simplification.md to state both language-specific APIs: keep Rust references as alkahest_cas::experimental::{simplify_par, simplify_redex}, and identify the Python functions as alkahest.simplify_par and alkahest.simplify_redex rather than placing them under alkahest.experimental.docs/mdbook/src/smt.md-94-102 (1)
94-102: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winCorrect the witness and
nlsatstatements.
decidereturns a verified rational witness only when one is available. A satisfied existential can returnwitness=Nonewhen its solution is irrational. Replace “a verified witness” with “an optional verified rational witness.”- Scope
nlsatcompleteness to quantifier-freeQF_LRA/QF_NRA.smt.solverejects quantified formulas;to_smtlibexports them, anddecidehandles quantifier elimination within its fragment.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/mdbook/src/smt.md` around lines 94 - 102, Update the SMT documentation paragraph around `decide` and `nlsat`: describe `decide` as returning an optional verified rational witness, since irrational solutions may produce `witness=None`, and limit the completeness claim for `nlsat` to quantifier-free `QF_LRA`/`QF_NRA`. Clarify that `smt.solve` rejects quantified formulas while `to_smtlib` exports them and `decide` performs quantifier elimination within its supported fragment.TESTING.md-82-82 (1)
82-82: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winRemove the blank line inside the blockquote.
markdownlintreports MD028 on Line 82. Keep the sanitizer note in one continuous blockquote.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@TESTING.md` at line 82, Remove the blank line within the sanitizer note blockquote in TESTING.md so the entire note remains one continuous blockquote and satisfies markdownlint MD028.Source: Linters/SAST tools
docs/sphinx/api/errors.rst-50-54 (1)
50-54: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick winInclude all documented refusal codes.
alkahest-skill/alkahest.mdLine 1125 classifiesE-LIMIT-003/005as refusals, but this list omits them. Add the codes or state that the list is non-exhaustive. Otherwise, callers can treat a limit refusal as a verdict.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/sphinx/api/errors.rst` around lines 50 - 54, Update the documented Refusals list in the errors reference to include E-LIMIT-003 and E-LIMIT-005, matching their classification in alkahest.md; alternatively, explicitly label the list non-exhaustive, while preserving the existing Verdicts classification.docs/features.md-177-179 (1)
177-179: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick winKeep the refusal-code list consistent.
This list omits
E-INT-001andE-LIMIT-003/005, which are documented as refusals inalkahest-skill/alkahest.md. Add the missing codes or state that the list is illustrative.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/features.md` around lines 177 - 179, Update the refusal-code documentation in docs/features.md to include E-INT-001 and E-LIMIT-003/005, keeping it consistent with the refusal codes documented in alkahest-skill/alkahest.md; alternatively, explicitly label the existing list as illustrative.docs/sphinx/api/workload.rst-63-67 (1)
63-67: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winDocument
budgetas required.The implementation requires the keyword-only
budgetargument, but the RST signature advertisesbudget=None. A caller that follows the documentation receivesTypeErrorbeforerun_with_wall_fallbackstarts.Change the RST signature to
budgetwithout a default.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/sphinx/api/workload.rst` around lines 63 - 67, Update the RST signature for run_with_wall_fallback to declare the keyword-only budget argument without a None default, matching the implementation’s required-argument contract.docs/mdbook/src/budgets.md-220-225 (1)
220-225: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winLimit the fallback guarantee to wall-clock overruns.
run_with_wall_fallbackraises whenfuture.result(timeout=...)times out. It does not report every silentsimplifybudget trip. Asimplifycall can return its best value aftermax_stepsor cancellation without timing out the worker. State that this helper reports wall-time overruns only.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/mdbook/src/budgets.md` around lines 220 - 225, Update the documentation for alkahest.run_with_wall_fallback to state that it raises BudgetExceededError only when the worker exceeds wall_ms; clarify that simplify may still return its best value after max_steps or cancellation without triggering this error.docs/mdbook/src/budgets.md-113-116 (1)
113-116: 🩺 Stability & Availability | 🟡 Minor | ⚡ Quick winScope the overshoot claim to the measured workload.
The text states that overshoot is not a function of problem size. The same section documents an uninterruptible FLINT operation that takes about two seconds for a degree-62 integrand. State that the additive behavior applies to the measured
n=40, d=17family. Checkpoint granularity can still grow with input size.Suggested wording
- is a small additive term, not a multiple of the budget and not a function of the - problem size. + was a small additive term for this measured family, not a multiple of the budget. + A high-degree primitive operation can still dominate the overshoot.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/mdbook/src/budgets.md` around lines 113 - 116, Revise the overshoot conclusion in the documented benchmark discussion to scope the additive behavior specifically to the measured n=40, d=17 workload family. Remove the broad claim that overshoot is independent of problem size, while preserving the reported measurements and acknowledging that checkpoint granularity may increase for larger inputs.
🧹 Nitpick comments (9)
alkahest-core/src/matrix/mod.rs (3)
298-311: 🚀 Performance & Scalability | 🔵 Trivial | 💤 Low valueConsider simplifying entries before the numeric test.
numeric_entriesmatches only literalIntegerandRationalnodes. A matrix built with unevaluated numeric entries, for examplepool.add(vec![one, two]), returnsNoneand falls back to theO(n!)cofactor path even though the matrix is numeric.detalready simplifies at the end of the symbolic path, so simplifying each entry here keeps the fast path reachable.♻️ Proposed change
- pool.with(e, |d| match d { + let e = simplify(e, pool).value; + pool.with(e, |d| match d {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/matrix/mod.rs` around lines 298 - 311, Update Matrix::numeric_entries to simplify each matrix entry through the expression pool before matching it as Integer or Rational, so unevaluated numeric expressions are recognized and converted to exact rationals. Preserve the existing None behavior for nonnumeric entries and keep det’s symbolic fallback unchanged.
360-366: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valuePublish or remove the performance-audit reference.
temp-alkahest/is ignored, and no trackedperformance-auditdocument exists. Move the audit todocs/or remove the reference.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/matrix/mod.rs` around lines 360 - 366, Update the determinant documentation near the `det_numeric` reference to remove the nonexistent `temp-alkahest/testing/3.8-performance-audit.md` link, or replace it with the corresponding tracked document under `docs/` if the audit is published there.
313-358: 🚀 Performance & Scalability | 🔵 Trivial | 💤 Low valueUse a specialized integer Bareiss path for integer matrices.
numeric_entriesconverts integer entries torug::Rational, so integer inputs use rational arithmetic throughout. Keep the rational path for fractional entries. The manifest usesrug = "1", and the listedRationalAPIs are supported.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/matrix/mod.rs` around lines 313 - 358, Update det_numeric to detect all-integer entries and run Bareiss elimination using rug::Integer values, converting the final determinant through the existing pool integer path; retain the current rug::Rational implementation for matrices containing fractional entries. Reuse numeric_entries or the underlying entry classification to preserve existing numeric validation and pivot/sign behavior, and use supported rug Integer arithmetic APIs.tests/test_budget.py (1)
209-217: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low value
_hard_trig_integrandis defined twice. Both files declare the same integrand helper with the same formula and separately tuneddvalues. A future retune must change both copies, and a missed copy makes one file assert a budget trip that no longer happens.
tests/test_budget.py#L209-L217: move the helper into a shared test module orconftest.py, and keep the rebuilt-ladder note with it.tests/test_batch_workload.py#L313-L325: delete the local copy and import the shared helper.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_budget.py` around lines 209 - 217, The _hard_trig_integrand helper is duplicated across the tests. In tests/test_budget.py lines 209-217, move the helper and its rebuilt-ladder note into a shared test module or conftest.py; in tests/test_batch_workload.py lines 313-325, delete the local definition and import the shared helper.alkahest-core/src/simplify/rules.rs (1)
156-204: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winConsider sharing one zero-to-negative-power predicate across subsystems.
alkahest-core/src/sum/mod.rsLines 196-216 definescontains_zero_to_negative_powerwith the same core test: a literal zero base under a negativeIntegerorRationalexponent.alkahest-core/src/simplify/egraph.rsLines 281-326 defines a third variant. The three copies already differ in which exponent literal types they accept.Export one predicate for the literal test, and keep only the traversal strategy local to each caller. This prevents the copies from diverging further and keeps the refusal semantics uniform.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/simplify/rules.rs` around lines 156 - 204, Extract and export a shared predicate for detecting a literal zero base raised to a negative literal exponent, then update the simplify, sum, and egraph callers to reuse it. Keep each caller’s existing traversal strategy local, while consolidating the exponent-type handling and refusal semantics in the shared predicate.alkahest-core/src/integrate/engine.rs (2)
3233-3248: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueRename the control test to match what it asserts.
u_substitution_still_declines_without_erroringasserts thatintegratesucceeds and returnssin(x² + 1). It does not assert a decline. The docstring explains the intent correctly — earlier candidates decline before the right one is found — but the name states the opposite of the assertion.♻️ Proposed rename
- fn u_substitution_still_declines_without_erroring() { + fn u_substitution_still_succeeds_after_earlier_candidates_decline() {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/engine.rs` around lines 3233 - 3248, Rename the test function u_substitution_still_declines_without_erroring to reflect that integration succeeds after earlier candidates decline, while preserving its existing assertions and test behavior.
3198-3229: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winGuard the wall-budget test against silently ceasing to test anything.
The doc comment records that this exact test stopped exercising a budget trip once
(12, 9)became fast enough, and that(40, 31)was chosen to restore it. The same decay will recur after the next performance improvement, and the test will still pass becauseexpect_errwould then fail loudly — no, it would fail, not pass. The real risk is the opposite direction: the assertion is only meaningful while the integrand stays slow, and nothing records the expected unbudgeted cost.Consider asserting the parameters are still hard by pinning the intent in a second control that runs the same integrand with a generous budget and asserts it does not trip. That makes the pair self-documenting and turns a future speedup into an explicit signal rather than a silent parameter bump.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/engine.rs` around lines 3198 - 3229, Strengthen a_wall_budget_stops_the_weierstrass_route_honestly by adding a control run of the same hard_trig_integrand parameters under a generous wall budget, asserting it completes without a budget error. Keep the existing 50 ms budget assertion and use the control to document that the chosen (40, 31) case remains genuinely expensive rather than merely unsupported.alkahest-core/src/integrate/risch/rational_rde.rs (2)
188-204: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winCorrect the stale "Why it is worth having" doc block.
Lines 190-197 describe the ℚ-Euclid remainder sequence and claim per-step granularity: "Checking once per Euclidean step makes the granularity one
poly_divrem." The body comment on lines 199-201 states the opposite, becausepoly_gcdnow delegates to FLINT and this function performs exactly one check before a single uninterruptible call. Two adjacent comments in the same function contradict each other. Update the doc block so the documented interruption granularity matches the implementation.♻️ Proposed doc correction
/// # Why it is worth having /// -/// The Euclidean algorithm over ℚ has no modular or fraction-free strategy here, -/// so the coefficients grow through the remainder sequence. Normalising `A/D` to -/// lowest terms in [`super::rational_integrate::try_integrate_rational`] -/// measured **480 ms of a 482 ms call** on the degree-80 image that -/// `∫ cos x·sin⁴⁰x/(sin¹⁷x + sin x + 1) dx` produces after the Weierstrass -/// substitution — the last uninterruptible block on that route once the other -/// checkpoints were in, and the reason a 50 ms budget still took 400 ms. -/// Checking once per Euclidean step makes the granularity one `poly_divrem`. +/// Normalising `A/D` to lowest terms in +/// [`super::rational_integrate::try_integrate_rational`] measured **480 ms of a +/// 482 ms call** under the previous ℚ-Euclid implementation, on the degree-80 +/// image that `∫ cos x·sin⁴⁰x/(sin¹⁷x + sin x + 1) dx` produces after the +/// Weierstrass substitution. It was the last uninterruptible block on that +/// route once the other checkpoints were in. +/// +/// `poly_gcd` now delegates to FLINT, so this function cannot interrupt the GCD +/// itself: the granularity is one whole `poly_gcd` call. That is acceptable +/// because the FLINT call is orders of magnitude shorter than the ℚ-Euclid it +/// replaced. pub(crate) fn poly_gcd_budgeted(a: &QPoly, b: &QPoly) -> Option<QPoly> { - // `poly_gcd` now delegates to FLINT, which is a single uninterruptible call - // — but one that is orders of magnitude shorter than the ℚ-Euclid it - // replaced, so the checkpoint before it is the granularity that matters. crate::budget::check().ok()?; Some(poly_gcd(a, b)) }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/risch/rational_rde.rs` around lines 188 - 204, Update the “Why it is worth having” documentation above poly_gcd_budgeted to describe the current FLINT-backed single-call implementation, including that this function performs one budget check before one uninterruptible poly_gcd call. Remove the stale ℚ-Euclid remainder-sequence, per-step poly_divrem, and outdated performance claims while preserving the function’s behavior.
1012-1016: 🎯 Functional Correctness | 🔵 TrivialKeep the direct equality assertions.
poly_monictrims its input, so both GCD results use canonical coefficient vectors. Runcargo fmtandcargo test --workspacebefore pushing.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/risch/rational_rde.rs` around lines 1012 - 1016, Preserve the direct equality assertion comparing poly_gcd and poly_gcd_euclid in the existing trial check; do not replace it with an indirect or normalized comparison. Run cargo fmt and cargo test --workspace to verify the change.Source: Coding guidelines
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@alkahest-core/src/ball/mod.rs`:
- Around line 362-377: Update the power-range logic around the corner validation
and min/max calculation: return an infinite-radius enclosure when any corner is
non-finite, not only when a corner is NaN, and explicitly detect a base interval
containing zero with a negative exponent and return the same unbounded result.
Correct the misleading comment, add regression tests for [0,0]^(-1) and
[-1,1]^(-1) through pow_f, and run cargo test --workspace.
In `@alkahest-core/src/integrate/risch/number_field.rs`:
- Around line 465-470: Update every algebraic RDE caller in exp_case.rs,
including the branches invoking solve_rational_rde_k, so budget cancellation is
checked with crate::budget::check()? before mapping a solver None to
Err(non_elementary()). Preserve genuine solver declines as NonElementary while
propagating budget errors, and apply the same distinction to all callers that
certify None as non-elementary.
In `@alkahest-core/src/poly/real_roots.rs`:
- Around line 758-795: After the bisection loop in the rational-root recovery
flow, verify that hi - lo is below target before computing scaled_lo/scaled_hi
or enumerating candidates. If the bound was not met, return None immediately;
otherwise preserve the existing candidate enumeration through n <= n_max.
In `@alkahest-core/src/simplify/egraph.rs`:
- Around line 937-942: Move the has_provably_zero_denominator(expr, pool) check
in the simplify flow to after the node_limit guard, so oversized inputs are
rejected before any zero_status/ArbBall scans run. Update the related doc
comment near the node-limit logic to describe the scan cost and its position
after the size check.
In `@alkahest-core/src/simplify/rules.rs`:
- Around line 206-213: Unify the literal zero-base/negative-exponent predicate
used by the simplify paths: in alkahest-core/src/simplify/rules.rs lines
156-204, extract the shared base/exponent test while keeping traversal depth
local to each caller; update is_negative_literal at lines 206-213 to treat
ExprData::Float values with f.inner < 0.0 as negative; and in
alkahest-core/src/simplify/egraph.rs lines 303-320 classify zero-valued
ExprData::Rational as Quick::Zero rather than Quick::NonZero.
In `@alkahest-py/src/lib.rs`:
- Around line 3532-3539: Update the limit path around core_limit to ensure the
pool_py PyRef borrow is dropped before entering py.allow_threads: extract the
inner pool reference or required pool data within a shorter borrow scope, then
call core_limit only after pool_ref is out of scope. Match the borrowing pattern
used by py_integrate.
- Around line 3364-3371: Update the integration flow around pool_ref and the
corresponding py_limit logic so the PyRef borrow is fully dropped before calling
py.allow_threads. Extract or clone the needed pool data into an owned,
thread-safe value within the GIL-held scope, then pass that value to
core_integrate without retaining pool_ref across the GIL release.
In `@docs/features.md`:
- Line 186: The feature documentation entry for
Budget/context/request_cancel/batch_map/*_many must qualify its workload
guarantee as “cooperatively bounded and cancellable,” replacing the current
“bounded, cancellable” wording while preserving the non-aborting fan-out
description.
In `@docs/mdbook/src/interop.md`:
- Around line 96-101: Update the SymPy description in the interop documentation
and the reference to tests/test_oracle.py to call SymPy an external comparison
or differential-testing oracle rather than a ground-truth reference. Preserve
the existing warning that branch-sensitive principal-branch evaluations may be
incomparable or non-eigenvalues.
- Around line 108-123: Correct the example around Matrix.eigenvals() by either
replacing the matrix with one whose irreducible cubic has three real roots, or
renaming the example to describe the actual one-real-root plus
complex-conjugate-pair result. Ensure the explanatory text and expected output
consistently match the chosen characterization.
In `@docs/sphinx/api/errors.rst`:
- Around line 50-54: Keep refusal-code classification consistent across all
three documentation sites: in docs/sphinx/api/errors.rst lines 50-54 and
docs/features.md lines 177-179, either add E-LIMIT-003 and E-LIMIT-005 plus
E-INT-001 where applicable or explicitly label the lists
illustrative/non-exhaustive; in docs/mdbook/src/batch.md lines 152-170, update
the batch handling so E-INT-001 and other refusal codes are routed to undecided
or retry handling rather than treated as definitive results.
In `@python/alkahest/_budget.py`:
- Around line 357-386: The cancellation restoration in the surrounding timeout
flow must not clear a cancellation request that arrived after this call set the
flag. Replace the separate is_cancelled()/clear_cancel() ownership check around
requested_here with an atomic compare-and-clear or equivalent generation-based
ownership mechanism, preserving pre-existing and concurrent cancellation
requests.
In `@TESTING.md`:
- Around line 144-146: Update the Valgrind instructions in TESTING.md to compile
alkahest-cas test binaries before the loop using cargo +nightly test -p
alkahest-cas --lib --tests --no-run, preserving the existing target and
RUSTFLAGS settings. Replace or supplement the workspace build so the
alkahest_cas-* binaries exist before Valgrind runs.
---
Minor comments:
In `@alkahest-core/src/simplify/egraph.rs`:
- Around line 303-320: Update the ExprData::Rational branch in the quick
classification match to inspect the rational numerator and return Quick::Zero
when r.0 == 0; keep nonzero rationals classified as Quick::NonZero so
negative-exponent handling reaches is_zero_denominator correctly.
In `@CONTRIBUTING.md`:
- Around line 34-40: Update the documented ASan command in CONTRIBUTING.md to
include LSAN_OPTIONS=detect_leaks=0 alongside RUSTFLAGS, preserving the existing
cargo package, target, and build-std arguments so it matches the CI environment.
In `@docs/features.md`:
- Around line 177-179: Update the refusal-code documentation in docs/features.md
to include E-INT-001 and E-LIMIT-003/005, keeping it consistent with the refusal
codes documented in alkahest-skill/alkahest.md; alternatively, explicitly label
the existing list as illustrative.
In `@docs/mdbook/src/budgets.md`:
- Around line 220-225: Update the documentation for
alkahest.run_with_wall_fallback to state that it raises BudgetExceededError only
when the worker exceeds wall_ms; clarify that simplify may still return its best
value after max_steps or cancellation without triggering this error.
- Around line 113-116: Revise the overshoot conclusion in the documented
benchmark discussion to scope the additive behavior specifically to the measured
n=40, d=17 workload family. Remove the broad claim that overshoot is independent
of problem size, while preserving the reported measurements and acknowledging
that checkpoint granularity may increase for larger inputs.
In `@docs/mdbook/src/simplification.md`:
- Line 146: Update the documentation sentence in simplification.md to state both
language-specific APIs: keep Rust references as
alkahest_cas::experimental::{simplify_par, simplify_redex}, and identify the
Python functions as alkahest.simplify_par and alkahest.simplify_redex rather
than placing them under alkahest.experimental.
In `@docs/mdbook/src/smt.md`:
- Around line 96-97: Update the SMT documentation statement about decide’s
result to qualify that the verified witness is returned when available, while
preserving the existing verdict description. Ensure the text does not imply that
every true existential result includes a witness.
- Around line 94-102: Update the SMT documentation paragraph around `decide` and
`nlsat`: describe `decide` as returning an optional verified rational witness,
since irrational solutions may produce `witness=None`, and limit the
completeness claim for `nlsat` to quantifier-free `QF_LRA`/`QF_NRA`. Clarify
that `smt.solve` rejects quantified formulas while `to_smtlib` exports them and
`decide` performs quantifier elimination within its supported fragment.
In `@docs/sphinx/api/autoresearch.rst`:
- Around line 15-18: Update the refusal-code note in the autoresearch
documentation to describe the codes as a set of route-specific examples rather
than claiming each module has exactly one code. Use wording such as “examples
include” and ensure it does not imply that listed codes like E-ANSATZ-003,
E-XCHECK-002, and E-SMT-003 are exhaustive.
In `@docs/sphinx/api/errors.rst`:
- Around line 50-54: Update the documented Refusals list in the errors reference
to include E-LIMIT-003 and E-LIMIT-005, matching their classification in
alkahest.md; alternatively, explicitly label the list non-exhaustive, while
preserving the existing Verdicts classification.
In `@docs/sphinx/api/workload.rst`:
- Around line 63-67: Update the RST signature for run_with_wall_fallback to
declare the keyword-only budget argument without a None default, matching the
implementation’s required-argument contract.
In `@TESTING.md`:
- Line 82: Remove the blank line within the sanitizer note blockquote in
TESTING.md so the entire note remains one continuous blockquote and satisfies
markdownlint MD028.
In `@tests/silent_errors/corpus.py`:
- Around line 159-171: Update _witness_residual to raise ak.CadError without the
unsupported code keyword when decide returns no witness, preserving the existing
error message and residual calculation.
---
Nitpick comments:
In `@alkahest-core/src/integrate/engine.rs`:
- Around line 3233-3248: Rename the test function
u_substitution_still_declines_without_erroring to reflect that integration
succeeds after earlier candidates decline, while preserving its existing
assertions and test behavior.
- Around line 3198-3229: Strengthen
a_wall_budget_stops_the_weierstrass_route_honestly by adding a control run of
the same hard_trig_integrand parameters under a generous wall budget, asserting
it completes without a budget error. Keep the existing 50 ms budget assertion
and use the control to document that the chosen (40, 31) case remains genuinely
expensive rather than merely unsupported.
In `@alkahest-core/src/integrate/risch/rational_rde.rs`:
- Around line 188-204: Update the “Why it is worth having” documentation above
poly_gcd_budgeted to describe the current FLINT-backed single-call
implementation, including that this function performs one budget check before
one uninterruptible poly_gcd call. Remove the stale ℚ-Euclid remainder-sequence,
per-step poly_divrem, and outdated performance claims while preserving the
function’s behavior.
- Around line 1012-1016: Preserve the direct equality assertion comparing
poly_gcd and poly_gcd_euclid in the existing trial check; do not replace it with
an indirect or normalized comparison. Run cargo fmt and cargo test --workspace
to verify the change.
In `@alkahest-core/src/matrix/mod.rs`:
- Around line 298-311: Update Matrix::numeric_entries to simplify each matrix
entry through the expression pool before matching it as Integer or Rational, so
unevaluated numeric expressions are recognized and converted to exact rationals.
Preserve the existing None behavior for nonnumeric entries and keep det’s
symbolic fallback unchanged.
- Around line 360-366: Update the determinant documentation near the
`det_numeric` reference to remove the nonexistent
`temp-alkahest/testing/3.8-performance-audit.md` link, or replace it with the
corresponding tracked document under `docs/` if the audit is published there.
- Around line 313-358: Update det_numeric to detect all-integer entries and run
Bareiss elimination using rug::Integer values, converting the final determinant
through the existing pool integer path; retain the current rug::Rational
implementation for matrices containing fractional entries. Reuse numeric_entries
or the underlying entry classification to preserve existing numeric validation
and pivot/sign behavior, and use supported rug Integer arithmetic APIs.
In `@alkahest-core/src/simplify/rules.rs`:
- Around line 156-204: Extract and export a shared predicate for detecting a
literal zero base raised to a negative literal exponent, then update the
simplify, sum, and egraph callers to reuse it. Keep each caller’s existing
traversal strategy local, while consolidating the exponent-type handling and
refusal semantics in the shared predicate.
In `@tests/test_budget.py`:
- Around line 209-217: The _hard_trig_integrand helper is duplicated across the
tests. In tests/test_budget.py lines 209-217, move the helper and its
rebuilt-ladder note into a shared test module or conftest.py; in
tests/test_batch_workload.py lines 313-325, delete the local definition and
import the shared helper.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: 4368b3f9-fc96-4f42-911a-6f4570817425
📒 Files selected for processing (50)
ARCHITECTURE.mdCHANGELOG.mdCONTRIBUTING.mdREADME.mdTESTING.mdalkahest-core/src/ball/mod.rsalkahest-core/src/errors/codes.rsalkahest-core/src/integrate/engine.rsalkahest-core/src/integrate/risch/number_field.rsalkahest-core/src/integrate/risch/rational_integrate.rsalkahest-core/src/integrate/risch/rational_rde.rsalkahest-core/src/matrix/eigen.rsalkahest-core/src/matrix/linear_algebra.rsalkahest-core/src/matrix/mod.rsalkahest-core/src/poly/real_roots.rsalkahest-core/src/real/cad.rsalkahest-core/src/simplify/egraph.rsalkahest-core/src/simplify/rules.rsalkahest-py/src/lib.rsalkahest-skill/alkahest.mddocs/features.mddocs/mdbook/src/ansatz.mddocs/mdbook/src/batch.mddocs/mdbook/src/budgets.mddocs/mdbook/src/claim-graphs.mddocs/mdbook/src/crosscheck.mddocs/mdbook/src/derivations.mddocs/mdbook/src/errors.mddocs/mdbook/src/interop.mddocs/mdbook/src/kernel.mddocs/mdbook/src/positivity.mddocs/mdbook/src/python-api.mddocs/mdbook/src/rules.mddocs/mdbook/src/search-plumbing.mddocs/mdbook/src/simplification.mddocs/mdbook/src/smt.mddocs/mdbook/src/stability.mddocs/sphinx/api/autoresearch.rstdocs/sphinx/api/errors.rstdocs/sphinx/api/matrix.rstdocs/sphinx/api/workload.rstdocs/sphinx/index.rstpython/alkahest/_batch.pypython/alkahest/_budget.pypython/alkahest/crosscheck.pytests/silent_errors/corpus.pytests/test_batch_workload.pytests/test_budget.pytests/test_cad_decide.pytests/test_linear_algebra.py
Comment on lines
+362
to
377
| // Defence in depth: any remaining NaN corner (an overflow, or a base | ||
| // interval straddling zero with a negative exponent) makes the ordering | ||
| // partial, and `partial_cmp(...).unwrap()` would panic on it. | ||
| if corners.iter().any(|c| c.is_nan()) { | ||
| return ArbBall::infinity(prec); | ||
| } | ||
| let min = corners | ||
| .iter() | ||
| .min_by(|a, b| a.partial_cmp(b).unwrap()) | ||
| .min_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | ||
| .unwrap() | ||
| .clone(); | ||
| let max = corners | ||
| .iter() | ||
| .max_by(|a, b| a.partial_cmp(b).unwrap()) | ||
| .max_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | ||
| .unwrap() | ||
| .clone(); |
There was a problem hiding this comment.
🎯 Functional Correctness | 🔴 Critical | ⚡ Quick win
Infinite corners still produce a NaN radius, and the comment misstates the straddling-zero case.
Two problems remain after the NaN guard.
0^(-1)in MPFR is+∞, not NaN. Forself = [0, 0]and an exact integer exponent-1, all four corners are+∞. The guard at Line 365 does not fire. Thenmin == max == +∞, sodiff = max - minisNaNand the returned ball hasrad = NaN. A ball with a NaN radius fails everycontainstest, which converts a division by zero into a false negative answer instead of a refusal. This is the same silent-error class the PR targets.- The comment at Lines 362-364 states that a base interval straddling zero with a negative exponent yields a NaN corner. It does not. For
self = [-1, 1]and exponent-1, the corners are-1and1, both finite, so the function returns the finite ball[-1, 1]. The true range is unbounded because of the pole at0. The returned enclosure is unsound.
Guard on non-finite corners rather than NaN alone, and add an explicit pole check for a base interval that contains zero with a negative exponent.
🛡️ Proposed fix
- // Defence in depth: any remaining NaN corner (an overflow, or a base
- // interval straddling zero with a negative exponent) makes the ordering
- // partial, and `partial_cmp(...).unwrap()` would panic on it.
- if corners.iter().any(|c| c.is_nan()) {
+ // A base interval that reaches zero with a negative exponent has a
+ // pole inside it, so no finite enclosure exists. Corner evaluation
+ // would report a bounded ball that does not enclose the true range.
+ if lo <= 0 && hi >= 0 && exp.lo() < 0 {
+ return ArbBall::infinity(prec);
+ }
+ // Any non-finite corner (NaN from an invalid power, ±∞ from an
+ // overflow or a division by zero) makes the ordering partial and
+ // makes `max - min` indeterminate, which would yield a `NaN` radius.
+ if corners.iter().any(|c| !c.is_finite()) {
return ArbBall::infinity(prec);
}Add regression cases for pow_f at [0,0]^(-1) and [-1,1]^(-1), and run cargo test --workspace.
As per coding guidelines: "Run cargo test --workspace for Rust unit, proptest, and doctest".
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| // Defence in depth: any remaining NaN corner (an overflow, or a base | |
| // interval straddling zero with a negative exponent) makes the ordering | |
| // partial, and `partial_cmp(...).unwrap()` would panic on it. | |
| if corners.iter().any(|c| c.is_nan()) { | |
| return ArbBall::infinity(prec); | |
| } | |
| let min = corners | |
| .iter() | |
| .min_by(|a, b| a.partial_cmp(b).unwrap()) | |
| .min_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | |
| .unwrap() | |
| .clone(); | |
| let max = corners | |
| .iter() | |
| .max_by(|a, b| a.partial_cmp(b).unwrap()) | |
| .max_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | |
| .unwrap() | |
| .clone(); | |
| // A base interval that reaches zero with a negative exponent has a | |
| // pole inside it, so no finite enclosure exists. Corner evaluation | |
| // would report a bounded ball that does not enclose the true range. | |
| if lo <= 0 && hi >= 0 && exp.lo() < 0 { | |
| return ArbBall::infinity(prec); | |
| } | |
| // Any non-finite corner (NaN from an invalid power, ±∞ from an | |
| // overflow or a division by zero) makes the ordering partial and | |
| // makes `max - min` indeterminate, which would yield a `NaN` radius. | |
| if corners.iter().any(|c| !c.is_finite()) { | |
| return ArbBall::infinity(prec); | |
| } | |
| let min = corners | |
| .iter() | |
| .min_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | |
| .unwrap() | |
| .clone(); | |
| let max = corners | |
| .iter() | |
| .max_by(|a, b| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) | |
| .unwrap() | |
| .clone(); |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/ball/mod.rs` around lines 362 - 377, Update the power-range
logic around the corner validation and min/max calculation: return an
infinite-radius enclosure when any corner is non-finite, not only when a corner
is NaN, and explicitly detect a base interval containing zero with a negative
exponent and return the same unbounded result. Correct the misleading comment,
add regression tests for [0,0]^(-1) and [-1,1]^(-1) through pow_f, and run cargo
test --workspace.
Source: Coding guidelines
Comment on lines
+465
to
+470
| // Cooperative checkpoint, once per elimination step. Each step is a | ||
| // full `K`-multiplication per coefficient of `b`, over ℚ-coefficients | ||
| // that grow as the Euclidean remainder sequence goes on, so a single | ||
| // `kpoly_divrem` on a degree-18 minimal polynomial is seconds of | ||
| // uninterruptible work — see `kpoly_gcd`. | ||
| crate::budget::check().ok()?; |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | 🏗️ Heavy lift
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Trace kpoly_divrem consumers to every caller-visible mathematical verdict.
set -euo pipefail
# Direct and indirect consumers.
rg -n -C 6 'kpoly_divrem|kpoly_div_exact|kpoly_mod\b|kpoly_mod_inverse|kpoly_ext_gcd' --type=rust
# Sites that turn a None into a non-elementary certificate.
rg -n -C 8 'NonElementary' --type=rust
# Budget re-check sites, to see which of the above are covered.
rg -n -C 4 'budget::check' --type=rustRepository: alkahest-cas/alkahest
Length of output: 159
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- target files ---'
git ls-files 'alkahest-core/src/integrate/risch/number_field.rs' \
'alkahest-core/src/integrate/risch/rational_rde.rs'
printf '%s\n' '--- relevant symbols and budget checks ---'
rg -n -C 8 'kpoly_(divrem|div_exact|mod_inverse|mod|ext_gcd|gcd)|budget::check|NonElementary' \
alkahest-core/src/integrate/risch/number_field.rs \
alkahest-core/src/integrate/risch/rational_rde.rs || true
printf '%s\n' '--- target implementation ranges ---'
sed -n '430,720p' alkahest-core/src/integrate/risch/number_field.rsRepository: alkahest-cas/alkahest
Length of output: 45131
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- all K-polynomial call sites ---'
rg -n -C 5 '(\.|::)kpoly_(gcd|div_exact|mod|mod_inverse|ext_gcd|divrem)\s*\(' \
alkahest-core/src --type rust || true
printf '%s\n' '--- integration entry points and budget handling ---'
rg -n -C 12 'fn integrate_inner|integrate_inner\s*\(|budget::check|E-BUDGET|NonElementary|non-elementary' \
alkahest-core/src/integrate --type rust || true
printf '%s\n' '--- rational RDE solver definitions and callers ---'
rg -n -C 18 'fn solve_.*rde|solve_.*_k|kpoly_(gcd|div_exact|mod_inverse|mod|ext_gcd)' \
alkahest-core/src/integrate/risch/rational_rde.rs --type rust || trueRepository: alkahest-cas/alkahest
Length of output: 50380
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- K-polynomial calls outside number_field.rs ---'
rg -n 'kpoly_(gcd|div_exact|mod_inverse|mod|ext_gcd|divrem)\s*\(' \
alkahest-core/src/integrate/risch --type rust \
| grep -v 'number_field.rs' || true
printf '%s\n' '--- relevant budget and error flow ---'
rg -n -C 10 'fn integrate_inner|E-BUDGET|budget::check|NonElementary' \
alkahest-core/src/integrate/engine.rs \
alkahest-core/src/integrate/risch/mod.rs \
alkahest-core/src/budget.rs \
alkahest-core/src/integrate/risch/rational_rde.rs \
2>/dev/null || true
printf '%s\n' '--- solver definitions and None-to-NonElementary branches ---'
rg -n -C 8 'fn (solve|integrate).*rde|None\s*=>|NonElementary' \
alkahest-core/src/integrate/risch/rational_rde.rs \
| grep -E 'rational_rde.rs|kpoly|solve|NonElementary|None' \
| head -n 1000 || trueRepository: alkahest-cas/alkahest
Length of output: 50377
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- integrate_inner error/decline handling ---'
sed -n '2243,2310p' alkahest-core/src/integrate/engine.rs
printf '%s\n' '--- rational_integrate K-polynomial caller ---'
sed -n '450,525p' alkahest-core/src/integrate/risch/rational_integrate.rs
printf '%s\n' '--- K-rational integration functions and return types ---'
sed -n '130,330p' alkahest-core/src/integrate/risch/k_rational_integrate.rs
sed -n '330,455p' alkahest-core/src/integrate/risch/k_rational_integrate.rs
printf '%s\n' '--- callers of K-rational integration ---'
rg -n -C 10 'k_rational_integrate|try_integrate.*field|integrate.*field|alg_log_argument|solve_.*rde' \
alkahest-core/src/integrate --type rust \
| grep -v 'number_field.rs' | head -n 1200 || trueRepository: alkahest-cas/alkahest
Length of output: 50378
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- K-solver definitions and call sites ---'
rg -n 'solve_rational_rde_k|integrate_k_rational_with_logs|kpoly_' \
alkahest-core/src/integrate/risch --type rust \
| grep -v 'number_field.rs' | grep -v 'k_rational_integrate.rs' || true
printf '%s\n' '--- exp_case K-solver branches ---'
rg -n -C 14 'solve_rational_rde_k|integrate_k_rational_with_logs' \
alkahest-core/src/integrate/risch/exp_case.rs || true
printf '%s\n' '--- rational_rde K-solver implementation and budget checks ---'
rg -n -C 16 'pub\(crate\)? fn solve_rational_rde_k|fn solve_rational_rde_k|budget::check|None =>' \
alkahest-core/src/integrate/risch/rational_rde.rs || true
printf '%s\n' '--- all budget checks in Risch sources ---'
rg -n 'budget::check' alkahest-core/src/integrate/risch --type rust || trueRepository: alkahest-cas/alkahest
Length of output: 23413
Preserve budget cancellation in K-polynomial RDE callers
solve_rational_rde_k propagates kpoly_divrem budget trips as None. The algebraic RDE branches in exp_case.rs (lines 744–756 and 789–801) convert that same None directly to Err(non_elementary()). integrate_inner does not re-check this path because it only re-checks try_integrate_rational before fallback handling.
Add crate::budget::check()? before converting solver None into NonElementary, or preserve budget errors separately from mathematical declines. Apply the same fix to every caller that certifies None as non-elementary.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/integrate/risch/number_field.rs` around lines 465 - 470,
Update every algebraic RDE caller in exp_case.rs, including the branches
invoking solve_rational_rde_k, so budget cancellation is checked with
crate::budget::check()? before mapping a solver None to Err(non_elementary()).
Preserve genuine solver declines as NonElementary while propagating budget
errors, and apply the same distinction to all callers that certify None as
non-elementary.
Comment on lines
+758
to
+795
| // Narrow until at most one multiple of 1/lc can remain inside. | ||
| let target = rug::Rational::from((Integer::from(1), lc.clone())); | ||
| for _ in 0..RATIONAL_RECOVERY_BISECTIONS { | ||
| if hi.clone() - lo.clone() < target { | ||
| break; | ||
| } | ||
| let mid = (lo.clone() + hi.clone()) / rug::Rational::from(2); | ||
| let v = eval_coeffs_rational(coeffs, &mid); | ||
| if v == 0 { | ||
| return Some(mid); | ||
| } | ||
| if (v > 0) == lo_positive { | ||
| lo = mid; | ||
| } else { | ||
| hi = mid; | ||
| } | ||
| } | ||
|
|
||
| // Any rational root has denominator dividing `lc`, i.e. is `n/lc` for an | ||
| // integer `n`. At most two such points survive a bracket this narrow. | ||
| let scaled_lo = lo * rug::Rational::from((lc.clone(), Integer::from(1))); | ||
| let scaled_hi = hi * rug::Rational::from((lc.clone(), Integer::from(1))); | ||
| let (mut n, _) = scaled_lo | ||
| .numer() | ||
| .clone() | ||
| .div_rem_ceil(scaled_lo.denom().clone()); | ||
| let (n_max, _) = scaled_hi | ||
| .numer() | ||
| .clone() | ||
| .div_rem_floor(scaled_hi.denom().clone()); | ||
| while n <= n_max { | ||
| let candidate = rug::Rational::from((n.clone(), lc.clone())); | ||
| if eval_coeffs_rational(coeffs, &candidate) == 0 { | ||
| return Some(candidate); | ||
| } | ||
| n += 1; | ||
| } | ||
| None |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | ⚡ Quick win
Stop candidate enumeration when bisection does not meet its bound.
Line 788 enumerates every multiple of 1/lc in the remaining bracket. The loop does not verify that 512 bisections reduced the bracket below target. A sufficiently wide interval can therefore make n_max - n arbitrarily large and bypass the intended recovery budget.
Return None when hi - lo >= target after the bisection loop. This preserves the original bracket and bounds recovery work.
Proposed fix
for _ in 0..RATIONAL_RECOVERY_BISECTIONS {
if hi.clone() - lo.clone() < target {
break;
}
// ...
}
+ if hi.clone() - lo.clone() >= target {
+ return None;
+ }
// Any rational root has denominator dividing `lc`...📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| // Narrow until at most one multiple of 1/lc can remain inside. | |
| let target = rug::Rational::from((Integer::from(1), lc.clone())); | |
| for _ in 0..RATIONAL_RECOVERY_BISECTIONS { | |
| if hi.clone() - lo.clone() < target { | |
| break; | |
| } | |
| let mid = (lo.clone() + hi.clone()) / rug::Rational::from(2); | |
| let v = eval_coeffs_rational(coeffs, &mid); | |
| if v == 0 { | |
| return Some(mid); | |
| } | |
| if (v > 0) == lo_positive { | |
| lo = mid; | |
| } else { | |
| hi = mid; | |
| } | |
| } | |
| // Any rational root has denominator dividing `lc`, i.e. is `n/lc` for an | |
| // integer `n`. At most two such points survive a bracket this narrow. | |
| let scaled_lo = lo * rug::Rational::from((lc.clone(), Integer::from(1))); | |
| let scaled_hi = hi * rug::Rational::from((lc.clone(), Integer::from(1))); | |
| let (mut n, _) = scaled_lo | |
| .numer() | |
| .clone() | |
| .div_rem_ceil(scaled_lo.denom().clone()); | |
| let (n_max, _) = scaled_hi | |
| .numer() | |
| .clone() | |
| .div_rem_floor(scaled_hi.denom().clone()); | |
| while n <= n_max { | |
| let candidate = rug::Rational::from((n.clone(), lc.clone())); | |
| if eval_coeffs_rational(coeffs, &candidate) == 0 { | |
| return Some(candidate); | |
| } | |
| n += 1; | |
| } | |
| None | |
| // Narrow until at most one multiple of 1/lc can remain inside. | |
| let target = rug::Rational::from((Integer::from(1), lc.clone())); | |
| for _ in 0..RATIONAL_RECOVERY_BISECTIONS { | |
| if hi.clone() - lo.clone() < target { | |
| break; | |
| } | |
| let mid = (lo.clone() + hi.clone()) / rug::Rational::from(2); | |
| let v = eval_coeffs_rational(coeffs, &mid); | |
| if v == 0 { | |
| return Some(mid); | |
| } | |
| if (v > 0) == lo_positive { | |
| lo = mid; | |
| } else { | |
| hi = mid; | |
| } | |
| } | |
| if hi.clone() - lo.clone() >= target { | |
| return None; | |
| } | |
| // Any rational root has denominator dividing `lc`, i.e. is `n/lc` for an | |
| // integer `n`. At most two such points survive a bracket this narrow. | |
| let scaled_lo = lo * rug::Rational::from((lc.clone(), Integer::from(1))); | |
| let scaled_hi = hi * rug::Rational::from((lc.clone(), Integer::from(1))); | |
| let (mut n, _) = scaled_lo | |
| .numer() | |
| .clone() | |
| .div_rem_ceil(scaled_lo.denom().clone()); | |
| let (n_max, _) = scaled_hi | |
| .numer() | |
| .clone() | |
| .div_rem_floor(scaled_hi.denom().clone()); | |
| while n <= n_max { | |
| let candidate = rug::Rational::from((n.clone(), lc.clone())); | |
| if eval_coeffs_rational(coeffs, &candidate) == 0 { | |
| return Some(candidate); | |
| } | |
| n += 1; | |
| } | |
| None |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/poly/real_roots.rs` around lines 758 - 795, After the
bisection loop in the rational-root recovery flow, verify that hi - lo is below
target before computing scaled_lo/scaled_hi or enumerating candidates. If the
bound was not met, return None immediately; otherwise preserve the existing
candidate enumeration through n <= n_max.
Comment on lines
+937
to
+942
| // `0⁻¹` in the e-graph makes `(Num 0)` and `(Num 1)` the same e-class | ||
| // (see `has_provably_zero_denominator`); hand it to the rule engine, | ||
| // which leaves the undefined product unevaluated. | ||
| if has_provably_zero_denominator(expr, pool) { | ||
| return super::super::engine::simplify(expr, pool); | ||
| } |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🟠 Major | ⚡ Quick win
Run the zero-denominator scan after the node-limit check.
The scan runs before the node_limit guard at Lines 947-958. For every non-literal base under a negative literal exponent, is_zero_denominator calls crate::matrix::zero_test::zero_status, which performs ArbBall evaluations. The doc comment at Lines 270-272 justifies that cost against "building and saturating an entire egglog program". That justification does not hold on the node-limit-exceeded path, because no egglog program is built there. An oversized input now pays an unbounded number of zero_status calls before the cheap size guard rejects it, which defeats the purpose of node_limit.
Move the bail-out below the node_limit block.
♻️ Proposed reorder
- // `0⁻¹` in the e-graph makes `(Num 0)` and `(Num 1)` the same e-class
- // (see `has_provably_zero_denominator`); hand it to the rule engine,
- // which leaves the undefined product unevaluated.
- if has_provably_zero_denominator(expr, pool) {
- return super::super::engine::simplify(expr, pool);
- }
-
// Enforce the node limit before handing the expression to egglog.
// Saturation can materialise exponentially many equivalent forms, so a
// hard pre-check on input size prevents OOM on pathological inputs.
if let Some(limit) = config.node_limit {
let n = count_dag_nodes(expr, pool);
if n > limit {
let mut log = DerivationLog::new();
log.push(RewriteStep::simple(
"egraph_node_limit_exceeded",
expr,
expr,
));
return DerivedExpr::with_log(expr, log);
}
}
+
+ // `0⁻¹` in the e-graph makes `(Num 0)` and `(Num 1)` the same e-class
+ // (see `has_provably_zero_denominator`); hand it to the rule engine,
+ // which leaves the undefined product unevaluated. Runs after the size
+ // guard: `zero_status` is far more expensive than the DAG count.
+ if has_provably_zero_denominator(expr, pool) {
+ return super::super::engine::simplify(expr, pool);
+ }Update the doc comment at Lines 270-272 to match the new order.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/simplify/egraph.rs` around lines 937 - 942, Move the
has_provably_zero_denominator(expr, pool) check in the simplify flow to after
the node_limit guard, so oversized inputs are rejected before any
zero_status/ArbBall scans run. Update the related doc comment near the
node-limit logic to describe the scan cost and its position after the size
check.
Comment on lines
+206
to
+213
| /// Whether `expr` is a negative `Integer` or `Rational` literal. | ||
| fn is_negative_literal(expr: ExprId, pool: &ExprPool) -> bool { | ||
| pool.with(expr, |data| match data { | ||
| ExprData::Integer(n) => n.0 < 0, | ||
| ExprData::Rational(r) => r.0 < 0, | ||
| _ => false, | ||
| }) | ||
| } |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Three copies of the "literal zero to a negative literal power" predicate accept different literal types. This PR adds guards in two files, and alkahest-core/src/sum/mod.rs Lines 196-216 already holds a third copy. Because each copy enumerates ExprData variants independently, an expression refused by one path is given a value by another, which reproduces the silent error the PR removes.
alkahest-core/src/simplify/rules.rs#L206-L213: addExprData::Float(f) => f.inner < 0.0tois_negative_literal, so aFloatexponent is refused as it is inegraph.rs.alkahest-core/src/simplify/egraph.rs#L303-L320: classify a zero-valuedExprData::RationalasQuick::Zeroinstead ofQuick::NonZero.alkahest-core/src/simplify/rules.rs#L156-L204: extract one shared predicate for the literal base and exponent test, and keep only the traversal depth local to each caller.
📍 Affects 2 files
alkahest-core/src/simplify/rules.rs#L206-L213(this comment)alkahest-core/src/simplify/egraph.rs#L303-L320alkahest-core/src/simplify/rules.rs#L156-L204
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/simplify/rules.rs` around lines 206 - 213, Unify the
literal zero-base/negative-exponent predicate used by the simplify paths: in
alkahest-core/src/simplify/rules.rs lines 156-204, extract the shared
base/exponent test while keeping traversal depth local to each caller; update
is_negative_literal at lines 206-213 to treat ExprData::Float values with
f.inner < 0.0 as negative; and in alkahest-core/src/simplify/egraph.rs lines
303-320 classify zero-valued ExprData::Rational as Quick::Zero rather than
Quick::NonZero.
Comment on lines
+96
to
+101
| Alkahest's kernel does not import SymPy. Two supported bridges exist on top of it: | ||
| `alkahest.crosscheck.to_sympy` translates an `Expr` into a SymPy expression, and | ||
| [`alkahest.crosscheck`](./crosscheck.md) drives SymPy as a differential-testing oracle. | ||
| The test oracle in `tests/test_oracle.py` uses SymPy as a ground-truth reference. For | ||
| ad-hoc mixed workflows, converting through the string representation is fine. | ||
|
|
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
Describe SymPy as a comparison oracle, not ground truth.
The same section documents that principal-branch evaluation can produce a non-eigenvalue for a branch-sensitive expression. Calling SymPy a “ground-truth reference” contradicts that warning. Describe it as an external comparison oracle and preserve incomparable handling for branch-sensitive results.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/mdbook/src/interop.md` around lines 96 - 101, Update the SymPy
description in the interop documentation and the reference to
tests/test_oracle.py to call SymPy an external comparison or
differential-testing oracle rather than a ground-truth reference. Preserve the
existing warning that branch-sensitive principal-branch evaluations may be
incomparable or non-eigenvalues.
Comment on lines
+108
to
+123
| `Matrix.eigenvals()` on a 3×3 with an irreducible cubic characteristic polynomial and | ||
| three real roots returns the Cardano form, and in the *casus irreducibilis* one of the | ||
| cube-root radicands is negative: | ||
|
|
||
| ```python | ||
| import alkahest as ak | ||
|
|
||
| pool = ak.ExprPool() | ||
| I = pool.integer | ||
| M = ak.Matrix.from_rows([[I(2), I(0), I(-2)], [I(2), I(0), I(-1)], [I(1), I(1), I(2)]]) | ||
|
|
||
| for value in M.eigenvals(): | ||
| print(value) | ||
| # two conjugate-looking siblings, then: | ||
| # (4/3 + (sqrt(298/27) + -89/27)^(1/3) + (-89/27 + (-1 * sqrt(298/27)))^(1/3)) | ||
| ``` |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Correct the “casus irreducibilis” example.
For the shown matrix, det(λI - M) = λ³ - 4λ² + 7λ + 2. Its derivative, 3λ² - 8λ + 7, is strictly positive, so the polynomial has one real root and a complex-conjugate pair. It is not casus irreducibilis, which requires three real roots. Rename the example or replace the matrix.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/mdbook/src/interop.md` around lines 108 - 123, Correct the example
around Matrix.eigenvals() by either replacing the matrix with one whose
irreducible cubic has three real roots, or renaming the example to describe the
actual one-real-root plus complex-conjugate-pair result. Ensure the explanatory
text and expected output consistently match the chosen characterization.
Comment on lines
+50
to
+54
| Refusals: ``E-CAD-001``, ``E-LINALG-010``, ``E-MAT-004``, ``E-SOS-002``, | ||
| ``E-ANSATZ-003``, ``E-SMT-003``, ``E-INT-001``, ``E-BUDGET-001..003``. | ||
|
|
||
| Verdicts: ``E-INT-004`` (proven non-elementary), ``E-MAT-003`` (proven | ||
| singular), ``E-EVAL-009`` (undefined at this point). |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
Keep refusal-code classification consistent across the public documentation.
The refusal taxonomy is incomplete in two pages, and the batch example treats E-INT-001 as a definitive result. Use one complete refusal-code set, or label lists as illustrative.
docs/sphinx/api/errors.rst#L50-L54: addE-LIMIT-003/005or state that the list is non-exhaustive.docs/features.md#L177-L179: includeE-INT-001andE-LIMIT-003/005, or state that the list is illustrative.docs/mdbook/src/batch.md#L152-L170: routeE-INT-001and other refusal codes to undecided or retry handling.
📍 Affects 3 files
docs/sphinx/api/errors.rst#L50-L54(this comment)docs/features.md#L177-L179docs/mdbook/src/batch.md#L152-L170
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/sphinx/api/errors.rst` around lines 50 - 54, Keep refusal-code
classification consistent across all three documentation sites: in
docs/sphinx/api/errors.rst lines 50-54 and docs/features.md lines 177-179,
either add E-LIMIT-003 and E-LIMIT-005 plus E-INT-001 where applicable or
explicitly label the lists illustrative/non-exhaustive; in
docs/mdbook/src/batch.md lines 152-170, update the batch handling so E-INT-001
and other refusal codes are routed to undecided or retry handling rather than
treated as definitive results.
Comment on lines
+357
to
+386
| # The cancellation flag is process-wide and sticky, so a timeout here must | ||
| # not outlive this call: without the restore below, one expired candidate | ||
| # in a long search loop leaves `CANCELLED` set and *every* subsequent | ||
| # cooperative call in the process fails with E-BUDGET-003 forever. Only | ||
| # restore a flag this call raised — an orchestrator that had already | ||
| # requested cancellation keeps its request. | ||
| cancelled_before = is_cancelled() | ||
| requested_here = False | ||
| timed_out: concurrent.futures.TimeoutError | None = None | ||
| started = time.perf_counter() | ||
| pool = concurrent.futures.ThreadPoolExecutor(max_workers=1) | ||
| try: | ||
| future = pool.submit(_run_on_worker) | ||
| try: | ||
| return future.result(timeout=budget.wall_ms / 1000.0) | ||
| except concurrent.futures.TimeoutError as exc: | ||
| # Best-effort: ask any cooperative Rust checkpoint the call has | ||
| # reached (or will reach) to stop, since we can't stop the | ||
| # Python thread itself. | ||
| # Belt and braces alongside the worker's own budget frame: it also | ||
| # reaches checkpoints the frame cannot (Rayon workers the callee | ||
| # fanned out to, or a callee that shadowed our frame with a nested | ||
| # `context(budget=...)` of its own). | ||
| request_cancel() | ||
| raise _budget_exceeded( | ||
| f"[E-BUDGET-001] budget exceeded: wall-clock limit {budget.wall_ms} ms elapsed", | ||
| remediation=( | ||
| "raise Budget(wall_ms=...), or accept a heuristic/numeric result for this " | ||
| "candidate instead of an exact one" | ||
| ), | ||
| ) from exc | ||
| requested_here = True | ||
| timed_out = exc | ||
| finally: | ||
| # `shutdown(wait=True)` — the join this function is honest about, and | ||
| # the reason the flag can be restored safely: by the time we get here | ||
| # the call we cancelled has already observed the flag and stopped. | ||
| pool.shutdown(wait=True) | ||
| if requested_here and not cancelled_before: | ||
| clear_cancel() |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | 🏗️ Heavy lift
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check whether the native budget module exposes a compare-and-clear or generation counter.
set -euo pipefail
rg -n -C 8 'fn request_cancel|fn clear_cancel|fn is_cancelled|CANCELLED' --type=rustRepository: alkahest-cas/alkahest
Length of output: 159
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- Rust files ---'
git ls-files | grep -E '(^|/)(Cargo\.toml|.*\.rs)$' || true
printf '%s\n' '--- Cancellation symbols ---'
rg -n -C 12 'request_cancel|clear_cancel|is_cancelled|CANCELLED|cancel' \
-g '*.rs' -g '*.py' -g '*.toml' . || true
printf '%s\n' '--- Relevant Python implementation ---'
python_files=$(git ls-files 'python/alkahest/_budget.py')
for file in $python_files; do
sed -n '330,400p' "$file"
doneRepository: alkahest-cas/alkahest
Length of output: 50380
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- Budget-related files ---'
rg --files | rg '(^|/)(budget|_budget)([^/]*)?$|budget\.(rs|py)$' || true
printf '%s\n' '--- Native cancellation definitions and call sites ---'
rg -n -C 15 'pub fn (request_cancel|clear_cancel|is_cancelled)|fn (request_cancel|clear_cancel|is_cancelled)|static .*CANCELLED|CANCELLED\.' \
-g '*.rs' . || true
printf '%s\n' '--- Python budget definitions and wrapper ---'
sed -n '1,120p' python/alkahest/_budget.py
sed -n '330,400p' python/alkahest/_budget.pyRepository: alkahest-cas/alkahest
Length of output: 13119
Use an atomic compare-and-clear for cancellation.
CANCELLED is an AtomicBool, but is_cancelled() and clear_cancel() are separate operations. A cancellation request can arrive after the check and before clear_cancel(), so this code can erase another thread’s request. Add a native compare-and-clear or generation-based ownership mechanism. A second read only narrows the race window.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@python/alkahest/_budget.py` around lines 357 - 386, The cancellation
restoration in the surrounding timeout flow must not clear a cancellation
request that arrived after this call set the flag. Replace the separate
is_cancelled()/clear_cancel() ownership check around requested_here with an
atomic compare-and-clear or equivalent generation-based ownership mechanism,
preserving pre-existing and concurrent cancellation requests.
Comment on lines
+144
to
+146
| # The crate's test binaries are `alkahest_cas-*` (package `alkahest-cas`). | ||
| # `alkahest_core-*` matches nothing and the guard below turns that into a silent pass. | ||
| for bin in target/x86_64-unknown-linux-gnu/debug/deps/alkahest_cas-*; do |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -eu
printf '%s\n' '--- TESTING.md context ---'
sed -n '120,165p' TESTING.md
printf '%s\n' '--- workspace manifests ---'
find . -name Cargo.toml -not -path '*/target/*' -print
printf '%s\n' '--- relevant Cargo commands and package names ---'
rg -n -C 4 'alkahest_cas|cargo \+nightly (build|test)|valgrind|x86_64-unknown-linux-gnu|sanitizer' TESTING.md .github Cargo.toml '*/Cargo.toml' 2>/dev/null || true
printf '%s\n' '--- Rust test targets ---'
find . -type f \( -name '*.rs' -o -name 'Cargo.toml' \) -not -path '*/target/*' -print | sort | head -200Repository: alkahest-cas/alkahest
Length of output: 26023
🏁 Script executed:
#!/bin/bash
set -eu
printf '%s\n' '--- package metadata ---'
sed -n '1,100p' Cargo.toml
sed -n '1,100p' alkahest-core/Cargo.toml
printf '%s\n' '--- test-related tracked files ---'
git ls-files | awk '
/(^|\/)tests?\// || /(^|\/)[^/]*_test[^/]*\.rs$/ || /(^|\/)test[^/]*\.rs$/ {
print
}
' | head -200
printf '%s\n' '--- test attributes and integration modules ---'
rg -n '(^|[^[:alnum:]_])#\[cfg\(test\)|(^|[^[:alnum:]_])#\[test\]|(^|/)tests?/' \
alkahest-core alkahest-py alkahest-mlir Cargo.toml alkahest-core/Cargo.toml \
--glob '*.rs' --glob 'Cargo.toml' | head -200
printf '%s\n' '--- Cargo command capabilities ---'
cargo --version
cargo test --help | sed -n '/--tests/,/--no-run/p'
cargo build --help | sed -n '/--tests/,/--profile/p'Repository: alkahest-cas/alkahest
Length of output: 22554
🏁 Script executed:
#!/bin/bash
set -eu
python3 - <<'PY'
from pathlib import Path
import glob
import re
import tomllib
root = Path(".")
manifest = tomllib.loads(Path("Cargo.toml").read_text())
package = tomllib.loads(Path("alkahest-core/Cargo.toml").read_text())
print("--- workspace/package identity ---")
print("workspace members:", manifest["workspace"]["members"])
print("package name:", package["package"]["name"])
print("package directory: alkahest-core")
print("--- Rust test targets in alkahest-core ---")
for path in sorted(Path("alkahest-core").rglob("*.rs")):
text = path.read_text(errors="replace")
if re.search(r"#\[test\]|#\[cfg\s*\(\s*test\s*\)", text):
print(path)
print("--- integration-test source files ---")
for path in sorted(Path("alkahest-core/tests").glob("*.rs")):
print(path)
print("--- pre-existing matching binaries ---")
pattern = "target/x86_64-unknown-linux-gnu/debug/deps/alkahest_cas-*"
matches = glob.glob(pattern)
print("pattern:", pattern)
print("matches:", matches)
print("matches_with_executable_bit:",
[p for p in matches if Path(p).is_file() and Path(p).stat().st_mode & 0o111])
print("--- command comparison ---")
print("build command creates ordinary targets only:", "--tests" not in
"cargo +nightly build --workspace --target x86_64-unknown-linux-gnu -Z build-std")
print("test command requests lib and integration test targets:", all(flag in
"cargo +nightly test -p alkahest-cas --lib --tests --no-run --target x86_64-unknown-linux-gnu -Z build-std"
for flag in ("--lib", "--tests", "--no-run")))
PYRepository: alkahest-cas/alkahest
Length of output: 279
🌐 Web query:
Official Cargo documentation for whether cargo buildbuilds test executables by default, and whethercargo test --lib --tests --no-run compiles test binaries without running them.
💡 Result:
According to the official Cargo documentation, the cargo build command does not compile test executables by default [1][2][3]. By default, cargo build compiles all library and binary targets of the selected packages [1][2][3]. To specifically include test targets during a build, you must use the --tests flag (or similar target selection flags like --test or --bench), which instructs Cargo to build all targets that have the test = true manifest flag set [1][2][3]. Regarding your second question, the command cargo test --lib --tests --no-run does indeed compile test binaries without executing them [4]. The --no-run flag explicitly tells Cargo to compile the tests but skip the execution phase [4]. When combined with --tests, it will build all test targets (including the library's unit tests and integration tests) [1][5][4], and adding the --lib flag restricts the scope to the package's library unit tests [6][7][4]. Therefore, this command sequence successfully prepares the test executables for you without running them [4].
Citations:
- 1: https://doc.rust-lang.org/stable/cargo/commands/cargo-build.html
- 2: https://dev-doc.rust-lang.org/cargo/commands/cargo-build.html
- 3: https://doc.rust-lang.org/cargo/commands/cargo-build.html
- 4: https://github.com/rust-lang/cargo/blob/master/src/etc/man/cargo-test.1
- 5: https://doc.rust-lang.org/stable/cargo/commands/cargo-test.html
- 6: https://stackoverflow.com/questions/69340746/cargo-says-test-failed-to-rerun-pass-lib-what-does-it-mean
- 7: https://stackoverflow.com/questions/34793506/how-to-run-library-tests-and-doc-tests-but-not-integration-tests
🏁 Script executed:
#!/bin/bash
set -eu
python3 - <<'PY'
from pathlib import Path
import glob
import re
workspace = Path("Cargo.toml").read_text()
core_manifest = Path("alkahest-core/Cargo.toml").read_text()
workspace_members = re.search(r'members\s*=\s*\[(.*?)\]', workspace, re.S)
package_name = re.search(r'(?m)^name\s*=\s*"([^"]+)"', core_manifest)
print("--- workspace/package identity ---")
print("workspace members:", workspace_members.group(1).replace("\n", " ").strip())
print("package name:", package_name.group(1))
print("--- Rust test targets in alkahest-core ---")
for path in sorted(Path("alkahest-core").rglob("*.rs")):
text = path.read_text(errors="replace")
if re.search(r"#\[test\]|#\[cfg\s*\(\s*test\s*\)", text):
print(path)
print("--- integration-test source files ---")
tests_dir = Path("alkahest-core/tests")
if tests_dir.is_dir():
for path in sorted(tests_dir.glob("*.rs")):
print(path)
print("--- matching binaries currently present ---")
pattern = "target/x86_64-unknown-linux-gnu/debug/deps/alkahest_cas-*"
matches = glob.glob(pattern)
print("pattern:", pattern)
print("matches:", matches)
print("executable matches:", [
path for path in matches
if Path(path).is_file() and Path(path).stat().st_mode & 0o111
])
print("--- command target-selection facts ---")
build = "cargo +nightly build --workspace --target x86_64-unknown-linux-gnu -Z build-std"
test = "cargo +nightly test -p alkahest-cas --lib --tests --no-run --target x86_64-unknown-linux-gnu -Z build-std"
print("build requests test targets:", "--tests" in build or "--test" in build)
print("test requests --lib:", "--lib" in test)
print("test requests --tests:", "--tests" in test)
print("test requests --no-run:", "--no-run" in test)
PYRepository: alkahest-cas/alkahest
Length of output: 7255
Compile the test binaries before running Valgrind.
cargo +nightly build --workspace does not compile test targets. On a clean checkout, alkahest_cas-* can match no files, so the guarded loop exits successfully without running Valgrind. Use cargo +nightly test -p alkahest-cas --lib --tests --no-run with the same target and RUSTFLAGS before the loop.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@TESTING.md` around lines 144 - 146, Update the Valgrind instructions in
TESTING.md to compile alkahest-cas test binaries before the loop using cargo
+nightly test -p alkahest-cas --lib --tests --no-run, preserving the existing
target and RUSTFLAGS settings. Replace or supplement the workspace build so the
alkahest_cas-* binaries exist before Valgrind runs.
…egfaults Round two of the pre-3.8 hunt. The validated-numerics finding is the one that matters most: the subsystem whose entire purpose is rigor was returning enclosures that do not contain the value they enclose. Validated numerics ------------------ Taylor models for `cos` and `tan` were negated. `bound_on_box(cos x, x in [1,1])` returned [-0.5403, -0.5403] — a *rigorous* enclosure excluding cos(1). Downstream that is not a wrong number but a false theorem: `verified_no_roots(cos x - 0.9, [0,1])` answered "true" although arccos(0.9) = 0.451 lies in the box. The cause is one line: `cos^(k) = sin^(k+1)` means the (k+1)%4 phase *is* the shift, and a further negation flipped the polynomial while leaving the symmetric remainder alone. sin^2 + cos^2 = 1 is invariant under that flip, which is exactly why the existing tests passed. `real_roots` silently dropped real roots: 25x^3 - 325x^2 + 804x - 540, which is 25(x - 6/5)(x - 9/5)(x - 10), reported one. `cf_lower_bound_floor` documented a false implication — equal signs at 0 and k imply an *even* count in between, not zero. It feeds `decide`, `solve` and the integrator's pole detector, so a dropped root propagates as a wrong verdict elsewhere. 2033 polynomials now agree with SymPy exactly. Also: a free parameter switched off every interior-pole guard, so the corpus's own archetype (integral of (x-a)^-2 over [-1,1]) returned -2 at a = 0; the pole scan was blind to tan/abs/atan because it sampled through a five-function evaluator, and blind to every simple pole because 1e30 is unreachable in doubles; the FTC was applied across discontinuous antiderivatives; `refine_root` returned balls provably not containing the root; and `guess_relation` rounded Python ints through f64 and then certified the result as exact. Process death ------------- Six ways to SIGSEGV, all unbounded recursion over the expression DAG, bisected in release: symbolic_grad at depth 4687, simplify and to_lean at 9472, latex at 12800, unicode_str at 15872, str at 24576. A crash is worse than a wrong answer for an unattended loop: nothing to catch, nothing in the log, the run dies. Fixed with a depth ceiling raising E-DEPTH-001. Depth is cached in `Node` at intern time beside the existing `mult_commutative` field and fits in its padding, so the check is an array read and a compare — measured at 0.976-1.043x across intern/str/latex/simplify/diff, inside the noise floor. Also a parser nesting cap, and `SEGMENT_BASE` re-baselining: it latched on a thread's first probe and never revisited, so a reused Rayon worker read its stack usage as zero however deep it went, then overflowed. Panics crossing the FFI boundary arrive as PanicException, which inherits BaseException and so slips past `except Exception` — the loop dies anyway. Closed in sparse_interp's user callback, six rug::Float precision paths, Matrix.get (which also wrapped r * cols and returned the wrong element), Budget(wall_ms=1e30), and two batch-evaluation length products that wrap in release. Eleven further silent errors are written up with call sites rather than half-fixed — `solve` returning spurious tuples and missing true ones, homotopy returning [] for a whole branch, `subresultant_prs` contradicting `resultant` — because a rushed fix days before a release is how the next one gets introduced. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…d-gil # Conflicts: # CHANGELOG.md
Merging this PR will not alter performance
Comparing 
Footnotes
|
There was a problem hiding this comment.
Actionable comments posted: 4
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
README.md (2)
125-128: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAlign the Rust crate version examples.
Change line 37 from
alkahest-cas = "2"toalkahest-cas = "3"to match the published crate version.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@README.md` around lines 125 - 128, Update the Rust crate version example near the earlier alkahest-cas dependency declaration from version "2" to version "3", matching the existing version shown in the feature example and the published crate version.
57-78: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winUse the published wheel filenames.
The
v3.7.0release providesmanylinux_2_35_x86_64wheels. The documentedlinux_x86_64URLs return 404. Update the examples and platform description to use the publishedmanylinux_2_35_x86_64filenames.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@README.md` around lines 57 - 78, Update the README’s Linux wheel platform description and both direct-install examples to use the published manylinux_2_35_x86_64 wheel tag instead of linux_x86_64. Preserve the existing version, Python ABI, local-version variants, and release URL structure while using the exact published wheel filenames so the documented links resolve.
🧹 Nitpick comments (2)
alkahest-core/src/integrate/engine.rs (2)
3573-3587: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueThe wall-clock test depends on timing and can flake.
a_wall_budget_stops_the_weierstrass_route_honestlyasserts that a 50 ms wall budget trips beforeintegratereturns. The assertion holds only while the search forn = 40, d = 31stays slower than 50 ms. Future performance work on the Weierstrass route could make the call finish first, and the test would then fail with a decline rather than a budget trip.Consider lowering the wall budget to a value that cannot be met (for example 1 ms), so the margin does not depend on the route's speed.
♻️ Proposed fix
let _guard = crate::budget::enter( - crate::budget::Budget::new().with_wall(std::time::Duration::from_millis(50)), + // Small enough that no plausible future speed-up lets the route + // finish first; the assertion is about the *reporting*, not the + // duration. + crate::budget::Budget::new().with_wall(std::time::Duration::from_millis(1)), );🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/engine.rs` around lines 3573 - 3587, Update the Budget configured in a_wall_budget_stops_the_weierstrass_route_honestly to use an effectively impossible wall-clock limit, such as 1 ms, so the test reliably exercises the budget-exceeded path regardless of Weierstrass route performance. Preserve the existing assertions for is_budget and E-BUDGET-001.
2711-2775: 🚀 Performance & Scalability | 🔵 Trivial | ⚡ Quick winAdd a cooperative budget checkpoint before each parameter assignment.
For four parameters, this loop tries 55 assignments. Each scan can perform 557
eval_interpcalls, for up to 30,635 expression evaluations.integrate_definiteruns this scan beforeintegrate, andeval_interphas no budget checkpoint. Wall-clock budgets and cancellation therefore cannot stop the scan at its current granularity.for assignment in assignments { + // Stop before the next scan when the caller's budget is spent. + if crate::budget::check().is_err() { + return None; + } let bindings: HashMap<ExprId, f64> = params🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@alkahest-core/src/integrate/engine.rs` around lines 2711 - 2775, Add a cooperative budget/cancellation checkpoint before processing each assignment in parametric_interior_singularity, using the existing integration budget mechanism and propagating its stop outcome from the function. Update the caller chain around integrate_definite as needed so an exhausted or cancelled budget terminates the scan promptly, while preserving the current singularity detection result for completed assignments.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@alkahest-core/src/integrate/engine.rs`:
- Around line 2634-2669: Update free_parameters to memoize visited ExprId nodes
and track discovered symbols in a separate set while preserving first-seen Vec
ordering; skip already visited nodes before recursion. At the start of
integrate_definite, validate all input expressions with the existing depth-check
mechanism before bound simplification or recursive traversal, and propagate the
resulting E-DEPTH-001 failure unchanged.
In `@alkahest-py/src/lib.rs`:
- Around line 1117-1141: Guard every expression-rendering representation against
excessive depth: update PyMatrix::__repr__, PySeries::__repr__/__str__,
PyODE::__repr__, PyDAE::__repr__, and PyHybridODE::__repr__ to return
PyResult<String>, call check_expr_depths for all contained expressions before
rendering, and propagate its error as DepthLimitError. Preserve the existing
rendering behavior after validation.
In `@tests/silent_errors/corpus.py`:
- Around line 2326-2359: Update the operations in cases sum_definite_keeps...
and product_definite_keeps... to pass the underlying DerivedResult.value into
_num, matching the surrounding sum/product cases. Preserve all existing case
metadata and expressions while ensuring the xfail cases evaluate the actual
numeric result directly.
---
Outside diff comments:
In `@README.md`:
- Around line 125-128: Update the Rust crate version example near the earlier
alkahest-cas dependency declaration from version "2" to version "3", matching
the existing version shown in the feature example and the published crate
version.
- Around line 57-78: Update the README’s Linux wheel platform description and
both direct-install examples to use the published manylinux_2_35_x86_64 wheel
tag instead of linux_x86_64. Preserve the existing version, Python ABI,
local-version variants, and release URL structure while using the exact
published wheel filenames so the documented links resolve.
---
Nitpick comments:
In `@alkahest-core/src/integrate/engine.rs`:
- Around line 3573-3587: Update the Budget configured in
a_wall_budget_stops_the_weierstrass_route_honestly to use an effectively
impossible wall-clock limit, such as 1 ms, so the test reliably exercises the
budget-exceeded path regardless of Weierstrass route performance. Preserve the
existing assertions for is_budget and E-BUDGET-001.
- Around line 2711-2775: Add a cooperative budget/cancellation checkpoint before
processing each assignment in parametric_interior_singularity, using the
existing integration budget mechanism and propagating its stop outcome from the
function. Update the caller chain around integrate_definite as needed so an
exhausted or cancelled budget terminates the scan promptly, while preserving the
current singularity detection result for completed assignments.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro Plus
Run ID: 8497bbf7-8874-4319-99eb-af8e36d6b23f
📒 Files selected for processing (19)
CHANGELOG.mdREADME.mdalkahest-core/src/errors/codes.rsalkahest-core/src/integrate/engine.rsalkahest-core/src/kernel/depth.rsalkahest-core/src/kernel/mod.rsalkahest-core/src/kernel/pool.rsalkahest-core/src/lib.rsalkahest-core/src/parse.rsalkahest-core/src/poly/real_roots.rsalkahest-core/src/simplify/parallel.rsalkahest-core/src/validated/taylor.rsalkahest-py/src/lib.rsdocs/features.mdpython/alkahest/__init__.pypython/alkahest/exceptions.pytests/silent_errors/corpus.pytests/test_expression_depth_limit.pytests/test_panic_boundary.py
🚧 Files skipped from review as they are similar to previous changes (2)
- docs/features.md
- alkahest-core/src/errors/codes.rs
Comment on lines
+2634
to
+2669
| /// Free symbols of `expr` other than `var`, in first-seen order. | ||
| /// | ||
| /// `∞` is excluded: it is the canonical bound marker, not a parameter, and it | ||
| /// is never a value the numeric evaluator could bind. | ||
| fn free_parameters(expr: ExprId, var: ExprId, pool: &ExprPool) -> Vec<ExprId> { | ||
| fn walk(e: ExprId, var: ExprId, inf: ExprId, pool: &ExprPool, out: &mut Vec<ExprId>) { | ||
| if e == var || e == inf { | ||
| return; | ||
| } | ||
| match pool.get(e) { | ||
| ExprData::Symbol { .. } => { | ||
| if !out.contains(&e) { | ||
| out.push(e); | ||
| } | ||
| } | ||
| ExprData::Add(xs) | ExprData::Mul(xs) => { | ||
| for x in xs { | ||
| walk(x, var, inf, pool, out); | ||
| } | ||
| } | ||
| ExprData::Pow { base, exp } => { | ||
| walk(base, var, inf, pool, out); | ||
| walk(exp, var, inf, pool, out); | ||
| } | ||
| ExprData::Func { args, .. } => { | ||
| for a in args { | ||
| walk(a, var, inf, pool, out); | ||
| } | ||
| } | ||
| _ => {} | ||
| } | ||
| } | ||
| let mut out = Vec::new(); | ||
| walk(expr, var, pool.pos_infinity(), pool, &mut out); | ||
| out | ||
| } |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check whether core entry points guard expression depth before recursing.
set -euo pipefail
# Locate the depth guard definition and every call site.
fd -t f 'depth.rs' alkahest-core/src/kernel --exec cat -n {}
rg -n --type=rust -C2 '\bcheck_expr_depth\s*\('
# Confirm integrate_definite has no depth guard on its own path.
ast-grep run --pattern $'pub fn integrate_definite($$$) -> $_ {
$$$
}' --lang rust alkahest-core/src/integrate/engine.rsRepository: alkahest-cas/alkahest
Length of output: 10356
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect the affected helper and definite-integration call paths.
sed -n '2320,2705p' alkahest-core/src/integrate/engine.rs
# Locate all uses of free_parameters and depth guards.
rg -n --type rust -C 4 'free_parameters|integrate_definite|check_expr_depth' alkahest-core/src
# Inspect the pool depth implementation and its sharing behavior.
rg -n --type rust -C 5 'fn depth|depth\(|hash.?cons|HashMap|HashSet' alkahest-core/src/kernel/pool.rs alkahest-core/src/kernelRepository: alkahest-cas/alkahest
Length of output: 50379
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Read the complete relevant implementations without the large test section.
sed -n '2695,2865p' alkahest-core/src/integrate/engine.rs
# Read the pool depth contract and node representation.
sed -n '1,90p' alkahest-core/src/kernel/pool.rs
sed -n '215,255p' alkahest-core/src/kernel/pool.rs
# Check whether integration itself performs a depth check or calls recursive
# expression walkers before the free-parameter checks.
rg -n --type rust -C 3 'pub fn integrate\(|fn integrate\(|pool\.get\(|match pool\.get|walk\(' \
alkahest-core/src/integrate/engine.rsRepository: alkahest-cas/alkahest
Length of output: 29005
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Model the exact no-visited-set traversal on a shared binary DAG.
python3 - <<'PY'
from functools import lru_cache
# A repeated-square DAG has one root whose two children are the same node.
# Each level therefore doubles path visits while adding only one node.
def path_visits(depth):
if depth == 0:
return 1
return 2 * path_visits(depth - 1)
`@lru_cache`(None)
def unique_nodes(depth):
return 1 if depth == 0 else 1 + unique_nodes(depth - 1)
for depth in (10, 20, 30, 40):
print(
f"depth={depth} unique_nodes={unique_nodes(depth)} "
f"unmemoised_visits={path_visits(depth)}"
)
PYRepository: alkahest-cas/alkahest
Length of output: 369
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Check how integrate_definite can return depth failures.
rg -n --type rust -C 6 'enum IntegrationError|struct IntegrationError|impl From<.*DepthLimitError|IntegrationError::NotImplemented|impl.*IntegrationError' \
alkahest-core/src/integrate alkahest-core/src/errors.rs alkahest-core/src
# Check the imports at the start of engine.rs.
sed -n '1,55p' alkahest-core/src/integrate/engine.rsRepository: alkahest-cas/alkahest
Length of output: 50378
Add memoization and a depth guard to integrate_definite
- Use a visited-node set and a separate symbol set in
free_parameters. Hash-consed shared subtrees can otherwise cause exponential traversal, andintegrate_definiteinvokes this helper up to three times. - Guard all inputs at the start of
integrate_definite, before bound simplification or recursive walkers. This entry point has nocheck_expr_depthcall, so deeply nested expressions can overflow the native stack. PreserveE-DEPTH-001when returning the depth failure.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-core/src/integrate/engine.rs` around lines 2634 - 2669, Update
free_parameters to memoize visited ExprId nodes and track discovered symbols in
a separate set while preserving first-seen Vec ordering; skip already visited
nodes before recursion. At the start of integrate_definite, validate all input
expressions with the existing depth-check mechanism before bound simplification
or recursive traversal, and propagate the resulting E-DEPTH-001 failure
unchanged.
Comment on lines
+1117
to
+1141
| // Every renderer below walks the expression recursively, so each one is a | ||
| // stack overflow — i.e. a `SIGSEGV`, not an exception — on a deep enough | ||
| // tree. `guard_depth` turns that into a catchable `DepthLimitError`. | ||
| fn __repr__(&self, py: Python<'_>) -> PyResult<String> { | ||
| let pool = self.pool.borrow(py); | ||
| guard_depth(&pool.inner, self.id)?; | ||
| Ok(pool.inner.display(self.id).to_string()) | ||
| } | ||
|
|
||
| fn __str__(&self, py: Python<'_>) -> String { | ||
| self.pool.borrow(py).inner.display(self.id).to_string() | ||
| fn __str__(&self, py: Python<'_>) -> PyResult<String> { | ||
| let pool = self.pool.borrow(py); | ||
| guard_depth(&pool.inner, self.id)?; | ||
| Ok(pool.inner.display(self.id).to_string()) | ||
| } | ||
|
|
||
| fn display_latex(&self, py: Python<'_>) -> String { | ||
| alkahest_core::render_latex(self.id, &self.pool.borrow(py).inner) | ||
| fn display_latex(&self, py: Python<'_>) -> PyResult<String> { | ||
| let pool = self.pool.borrow(py); | ||
| guard_depth(&pool.inner, self.id)?; | ||
| Ok(alkahest_core::render_latex(self.id, &pool.inner)) | ||
| } | ||
|
|
||
| fn display_unicode(&self, py: Python<'_>) -> String { | ||
| alkahest_core::render_unicode(self.id, &self.pool.borrow(py).inner) | ||
| fn display_unicode(&self, py: Python<'_>) -> PyResult<String> { | ||
| let pool = self.pool.borrow(py); | ||
| guard_depth(&pool.inner, self.id)?; | ||
| Ok(alkahest_core::render_unicode(self.id, &pool.inner)) |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Find remaining PyO3 renderers that walk expressions without a depth guard.
set -euo pipefail
# Every __repr__ / __str__ / display method in the bindings.
rg -nP --type=rust -C6 'fn\s+(__repr__|__str__|display_\w+)\s*\(' alkahest-py/src/lib.rs
# Cross-check which of them call guard_depth or check_expr_depths.
rg -nP --type=rust -C10 'fn\s+__repr__\s*\(' alkahest-py/src/lib.rs \
| rg -n 'guard_depth|check_expr_depths|fn __repr__'Repository: alkahest-cas/alkahest
Length of output: 18484
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect the matrix implementation and the depth-checking APIs.
sed -n '5660,5780p' alkahest-py/src/lib.rs
rg -n -C5 'fn\s+(check_expr_depths|guard_depth|guard_expr_depth)|check_expr_depths|struct\s+Matrix|impl\s+.*Matrix|fn\s+display' --glob '*.rs' .Repository: alkahest-cas/alkahest
Length of output: 41010
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '5660,5780p' alkahest-py/src/lib.rs
rg -n -C5 'fn\s+(check_expr_depths|guard_depth|guard_expr_depth)|check_expr_depths|struct\s+Matrix|impl\s+.*Matrix|fn\s+display' --glob '*.rs' .Repository: alkahest-cas/alkahest
Length of output: 41010
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Read the exact matrix display/get implementations and nearby expression-rendering wrappers.
sed -n '115,155p;560,590p' alkahest-core/src/matrix/mod.rs
sed -n '5120,5185p;1508,1535p;5960,5985p;6135,6160p;6245,6275p' alkahest-py/src/lib.rs
# Read-only behavioral/source-shape verifier for the stated call graph.
python3 - <<'PY'
from pathlib import Path
import re
matrix = Path("alkahest-core/src/matrix/mod.rs").read_text()
binding = Path("alkahest-py/src/lib.rs").read_text()
display = re.search(
r"impl Matrix \{\s*pub fn display\(&self, pool: &ExprPool\) -> String \{(?P<body>.*?)\n\s*\}\n\}",
matrix,
re.S,
)
assert display, "Matrix::display was not found"
body = display.group("body")
print("Matrix::display calls pool.display:", "pool.display(" in body)
print("Matrix::display calls self.row:", "self.row(" in body)
matrix_repr = re.search(
r"fn __repr__\(&self, py: Python<'_>\) -> String \{\s*"
r"let pool = self\.pool\.borrow\(py\);\s*"
r"self\.inner\.display\(&pool\.inner\)\s*\}",
binding,
re.S,
)
assert matrix_repr, "unhardened PyMatrix::__repr__ shape was not found"
print("PyMatrix::__repr__ has no depth check:", "guard_depth" not in matrix_repr.group(0)
and "check_expr_depths" not in matrix_repr.group(0))
check = re.search(
r"pub fn check_expr_depths\(pool: &ExprPool, ids: &\[ExprId\]\).*?"
r"\{\s*(?P<body>.*?)\n\}",
Path("alkahest-core/src/kernel/depth.rs").read_text(),
re.S,
)
assert check and "check_expr_depth(pool, id)" in check.group("body")
print("check_expr_depths checks each supplied ID:", True)
PYRepository: alkahest-cas/alkahest
Length of output: 8200
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '115,155p;560,590p' alkahest-core/src/matrix/mod.rs
sed -n '5120,5185p;1508,1535p;5960,5985p;6135,6160p;6245,6275p' alkahest-py/src/lib.rs
python3 - <<'PY'
from pathlib import Path
import re
matrix = Path("alkahest-core/src/matrix/mod.rs").read_text()
binding = Path("alkahest-py/src/lib.rs").read_text()
display = re.search(
r"impl Matrix \{\s*pub fn display\(&self, pool: &ExprPool\) -> String \{(?P<body>.*?)\n\s*\}\n\}",
matrix,
re.S,
)
assert display, "Matrix::display was not found"
body = display.group("body")
print("Matrix::display calls pool.display:", "pool.display(" in body)
print("Matrix::display calls self.row:", "self.row(" in body)
matrix_repr = re.search(
r"fn __repr__\(&self, py: Python<'_>\) -> String \{\s*"
r"let pool = self\.pool\.borrow\(py\);\s*"
r"self\.inner\.display\(&pool\.inner\)\s*\}",
binding,
re.S,
)
assert matrix_repr, "unhardened PyMatrix::__repr__ shape was not found"
print("PyMatrix::__repr__ has no depth check:", "guard_depth" not in matrix_repr.group(0)
and "check_expr_depths" not in matrix_repr.group(0))
check = re.search(
r"pub fn check_expr_depths\(pool: &ExprPool, ids: &\[ExprId\]\).*?"
r"\{\s*(?P<body>.*?)\n\}",
Path("alkahest-core/src/kernel/depth.rs").read_text(),
re.S,
)
assert check and "check_expr_depth(pool, id)" in check.group("body")
print("check_expr_depths checks each supplied ID:", True)
PYRepository: alkahest-cas/alkahest
Length of output: 8200
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect all binding methods that directly or indirectly render ExprPool entries.
sed -n '5145,5275p' alkahest-py/src/lib.rs
sed -n '5940,5990p;6100,6160p;6225,6280p' alkahest-py/src/lib.rs
sed -n '140,180p' alkahest-core/src/ode/mod.rs
sed -n '155,185p' alkahest-core/src/dae/mod.rs
sed -n '80,105p;160,185p' alkahest-core/src/hybrid/mod.rs
# Read-only verifier: identify unguarded binding methods whose display call
# reaches ExprPool::display through the core display implementations.
python3 - <<'PY'
from pathlib import Path
binding = Path("alkahest-py/src/lib.rs").read_text()
for name in ("PySeries", "PyMatrix", "PyODE", "PyDAE", "PyHybridODE"):
start = binding.find(f"impl {name}")
assert start >= 0, name
end = binding.find("\n}\n", start)
block = binding[start:end]
print(name)
for method in ("fn __repr__", "fn __str__"):
pos = block.find(method)
if pos >= 0:
method_end = block.find("\n }", pos)
snippet = block[pos:method_end]
print(" ", method, "has depth guard:",
"guard_depth" in snippet or "check_expr_depths" in snippet)
core = {
"Matrix": Path("alkahest-core/src/matrix/mod.rs").read_text(),
"ODE": Path("alkahest-core/src/ode/mod.rs").read_text(),
"DAE": Path("alkahest-core/src/dae/mod.rs").read_text(),
"Hybrid": Path("alkahest-core/src/hybrid/mod.rs").read_text(),
}
for name, text in core.items():
marker = "pub fn display"
pos = text.find(marker)
assert pos >= 0, name
body = text[pos:text.find("\n }\n", pos)]
print(f"{name} display reaches pool.display:", "pool.display(" in body)
PYRepository: alkahest-cas/alkahest
Length of output: 14266
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '5145,5275p' alkahest-py/src/lib.rs
sed -n '5940,5990p;6100,6160p;6225,6280p' alkahest-py/src/lib.rs
sed -n '140,180p' alkahest-core/src/ode/mod.rs
sed -n '155,185p' alkahest-core/src/dae/mod.rs
sed -n '80,105p;160,185p' alkahest-core/src/hybrid/mod.rs
python3 - <<'PY'
from pathlib import Path
binding = Path("alkahest-py/src/lib.rs").read_text()
for name in ("PySeries", "PyMatrix", "PyODE", "PyDAE", "PyHybridODE"):
start = binding.find(f"impl {name}")
assert start >= 0, name
end = binding.find("\n}\n", start)
block = binding[start:end]
print(name)
for method in ("fn __repr__", "fn __str__"):
pos = block.find(method)
if pos >= 0:
method_end = block.find("\n }", pos)
snippet = block[pos:method_end]
print(" ", method, "has depth guard:",
"guard_depth" in snippet or "check_expr_depths" in snippet)
core = {
"Matrix": Path("alkahest-core/src/matrix/mod.rs").read_text(),
"ODE": Path("alkahest-core/src/ode/mod.rs").read_text(),
"DAE": Path("alkahest-core/src/dae/mod.rs").read_text(),
"Hybrid": Path("alkahest-core/src/hybrid/mod.rs").read_text(),
}
for name, text in core.items():
marker = "pub fn display"
pos = text.find(marker)
assert pos >= 0, name
body = text[pos:text.find("\n }\n", pos)]
print(f"{name} display reaches pool.display:", "pool.display(" in body)
PYRepository: alkahest-cas/alkahest
Length of output: 14266
Guard all expression-rendering representations against excessive depth.
PyMatrix::__repr__ still calls Matrix::display, which recursively renders every entry without a depth guard. A deep entry can still cause a native stack overflow instead of raising DepthLimitError. Return PyResult<String> and call check_expr_depths for all matrix entries before rendering.
Apply the same guard to PySeries::__repr__/__str__, PyODE::__repr__, PyDAE::__repr__, and PyHybridODE::__repr__, which also render expressions without a guard (at lines 1523, 1528, 5758, 5977, 6149, and 6266).
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@alkahest-py/src/lib.rs` around lines 1117 - 1141, Guard every
expression-rendering representation against excessive depth: update
PyMatrix::__repr__, PySeries::__repr__/__str__, PyODE::__repr__,
PyDAE::__repr__, and PyHybridODE::__repr__ to return PyResult<String>, call
check_expr_depths for all contained expressions before rendering, and propagate
its error as DepthLimitError. Preserve the existing rendering behavior after
validation.
Comment on lines
+11183
to
+11186
| m.add( | ||
| "DepthLimitError", | ||
| m.py().get_type_bound::<PyDepthLimitError>(), | ||
| )?; |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check that the exported DepthLimitError matches the native one and that E-DEPTH-001 is documented.
set -euo pipefail
echo "=== Python re-export of DepthLimitError"
rg -n -C3 '\bDepthLimitError\b' python/alkahest/__init__.py python/alkahest/exceptions.py
echo "=== Native error code emitted"
rg -n -C6 'E-DEPTH' alkahest-core/src alkahest-py/src
echo "=== AlkahestError::code for DepthLimitError"
fd -t f 'depth.rs' alkahest-core/src/kernel --exec rg -n -C6 'fn code|E-DEPTH|impl .*AlkahestError' {}
echo "=== Documentation of the code"
rg -n 'E-DEPTH' docs/Repository: alkahest-cas/alkahest
Length of output: 10828
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "=== Python export and native-module imports"
sed -n '300,350p' python/alkahest/__init__.py
rg -n -C5 'DepthLimitError|depth_error_to_py|PyDepthLimitError|create_exception!' alkahest-py/src/lib.rs alkahest-py/src
echo "=== Error-code exposure in the native binding"
rg -n -C8 'E-DEPTH-001|code\(\)|setattr.*code|code' alkahest-py/src alkahest-core/src/errors
echo "=== Documentation files and error references"
git ls-files 'docs/**' | head -100
rg -n -C2 'E-[A-Z]+-[0-9]{3}|DepthLimitError' docs README.md python alkahest-py alkahest-coreRepository: alkahest-cas/alkahest
Length of output: 50380
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "=== __init__.py import order"
sed -n '1,80p' python/alkahest/__init__.py
sed -n '320,345p' python/alkahest/__init__.py
rg -n -C4 'from .*exceptions|from .*_alkahest|import \*|DepthLimitError' python/alkahest/__init__.py
echo "=== Native depth exception implementation and conversion"
rg -n -C10 'PyDepthLimitError|depth_error_to_py|DepthLimitError' alkahest-py/src/lib.rs
rg -n -C8 'create_exception!' alkahest-py/src/lib.rs
echo "=== Exact error reference entries"
rg -n -C4 -F 'E-DEPTH-001' docs/mdbook/src/errors.md docs || true
rg -n -C4 -F 'DepthLimitError' docs/mdbook/src/errors.md docs || trueRepository: alkahest-cas/alkahest
Length of output: 17953
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "=== Native class replacement in python/alkahest/__init__.py"
sed -n '418,455p' python/alkahest/__init__.py
echo "=== Structured error attributes"
sed -n '395,425p' alkahest-py/src/lib.rs
echo "=== Error reference structure near the refusal table"
sed -n '90,120p' docs/mdbook/src/errors.md
sed -n '145,185p' docs/mdbook/src/errors.mdRepository: alkahest-cas/alkahest
Length of output: 7365
🏁 Script executed:
#!/bin/bash
set -euo pipefail
rg -n -C8 '_NATIVE_EXCEPTION_OVERLAY' python/alkahest/__init__.pyRepository: alkahest-cas/alkahest
Length of output: 1062
Document E-DEPTH-001 in docs/mdbook/src/errors.md
Add DepthLimitError and its remediation to the error taxonomy. The package exports the native class, and depth_error_to_py sets .code to E-DEPTH-001; only the user-facing error reference is missing this code.
Source: Coding guidelines
Comment on lines
+2326
to
+2359
| Case( | ||
| id="sum_definite_interior_pole_refused", | ||
| subsystem="sums_products", | ||
| statement="Σ_{k=1}^{10} 1/((k-3)(k-2)) is undefined — the k=2 and k=3 terms divide by zero", | ||
| op=lambda: _num( | ||
| ak.sum_definite(((K - _int(3)) * (K - _int(2))) ** _int(-1), K, _int(1), _int(10)) | ||
| ), | ||
| contract=RefusesOr(), | ||
| verified_by=( | ||
| "The k=2 term is 1/((-1)·0) and the k=3 term is 1/(0·1); neither is a number, so the " | ||
| "sum has no value. alkahest returned -5/8. Its own docstring promises E-SUM-003 for " | ||
| "exactly this." | ||
| ), | ||
| xfail=( | ||
| "SILENT ERROR: sum_definite tests contains_zero_to_negative_power only on the " | ||
| "telescoped difference G(hi+1) - G(lo) (alkahest-core/src/sum/mod.rs:181), so a pole " | ||
| "strictly between the endpoints is invisible and only poles landing exactly on lo or " | ||
| "hi+1 are caught. See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | ||
| ), | ||
| ), | ||
| Case( | ||
| id="product_definite_keeps_rational_scale", | ||
| subsystem="sums_products", | ||
| statement="Π_{k=1}^{5} 1/2 = 1/32", | ||
| op=lambda: _num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5))), | ||
| contract=Returns(1.0 / 32.0, tol=1e-12), | ||
| verified_by="Five factors of 1/2 multiply to 2^-5 = 1/32, by the definition of a product.", | ||
| xfail=( | ||
| "SILENT ERROR: product_definite returns 1. ratuni_poly_to_univ " | ||
| "(alkahest-core/src/sum/product.rs:109-144) clears coefficient denominators by " | ||
| "multiplying through by their LCM and never returns or reapplies that scale, so the " | ||
| "answer is off by c^(hi-lo+1). See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | ||
| ), | ||
| ), |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Add the missing .value so these two cases match the surrounding pattern.
Line 2330 and Line 2350 pass the DerivedResult straight to _num:
_num(ak.sum_definite(...))_num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5)))
Every other sum and product case in this file unwraps first — Line 1871 _num(ak.sum_definite(...).value), Line 1897 and Line 1922 _num(ak.product_definite(...).value).
eval_expr does coerce a DerivedResult, so this probably works. The risk is specific to these two cases: both carry xfail, so if _num fails for an unrelated reason the case still reports as expected-fail and stops testing the documented defect. When the underlying bug is fixed, the case will not flip to a pass.
♻️ Proposed fix
op=lambda: _num(
- ak.sum_definite(((K - _int(3)) * (K - _int(2))) ** _int(-1), K, _int(1), _int(10))
+ ak.sum_definite(
+ ((K - _int(3)) * (K - _int(2))) ** _int(-1), K, _int(1), _int(10)
+ ).value
),- op=lambda: _num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5))),
+ op=lambda: _num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5)).value),📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| Case( | |
| id="sum_definite_interior_pole_refused", | |
| subsystem="sums_products", | |
| statement="Σ_{k=1}^{10} 1/((k-3)(k-2)) is undefined — the k=2 and k=3 terms divide by zero", | |
| op=lambda: _num( | |
| ak.sum_definite(((K - _int(3)) * (K - _int(2))) ** _int(-1), K, _int(1), _int(10)) | |
| ), | |
| contract=RefusesOr(), | |
| verified_by=( | |
| "The k=2 term is 1/((-1)·0) and the k=3 term is 1/(0·1); neither is a number, so the " | |
| "sum has no value. alkahest returned -5/8. Its own docstring promises E-SUM-003 for " | |
| "exactly this." | |
| ), | |
| xfail=( | |
| "SILENT ERROR: sum_definite tests contains_zero_to_negative_power only on the " | |
| "telescoped difference G(hi+1) - G(lo) (alkahest-core/src/sum/mod.rs:181), so a pole " | |
| "strictly between the endpoints is invisible and only poles landing exactly on lo or " | |
| "hi+1 are caught. See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | |
| ), | |
| ), | |
| Case( | |
| id="product_definite_keeps_rational_scale", | |
| subsystem="sums_products", | |
| statement="Π_{k=1}^{5} 1/2 = 1/32", | |
| op=lambda: _num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5))), | |
| contract=Returns(1.0 / 32.0, tol=1e-12), | |
| verified_by="Five factors of 1/2 multiply to 2^-5 = 1/32, by the definition of a product.", | |
| xfail=( | |
| "SILENT ERROR: product_definite returns 1. ratuni_poly_to_univ " | |
| "(alkahest-core/src/sum/product.rs:109-144) clears coefficient denominators by " | |
| "multiplying through by their LCM and never returns or reapplies that scale, so the " | |
| "answer is off by c^(hi-lo+1). See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | |
| ), | |
| ), | |
| Case( | |
| id="sum_definite_interior_pole_refused", | |
| subsystem="sums_products", | |
| statement="Σ_{k=1}^{10} 1/((k-3)(k-2)) is undefined — the k=2 and k=3 terms divide by zero", | |
| op=lambda: _num( | |
| ak.sum_definite( | |
| ((K - _int(3)) * (K - _int(2))) ** _int(-1), K, _int(1), _int(10) | |
| ).value | |
| ), | |
| contract=RefusesOr(), | |
| verified_by=( | |
| "The k=2 term is 1/((-1)·0) and the k=3 term is 1/(0·1); neither is a number, so the " | |
| "sum has no value. alkahest returned -5/8. Its own docstring promises E-SUM-003 for " | |
| "exactly this." | |
| ), | |
| xfail=( | |
| "SILENT ERROR: sum_definite tests contains_zero_to_negative_power only on the " | |
| "telescoped difference G(hi+1) - G(lo) (alkahest-core/src/sum/mod.rs:181), so a pole " | |
| "strictly between the endpoints is invisible and only poles landing exactly on lo or " | |
| "hi+1 are caught. See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | |
| ), | |
| ), | |
| Case( | |
| id="product_definite_keeps_rational_scale", | |
| subsystem="sums_products", | |
| statement="Π_{k=1}^{5} 1/2 = 1/32", | |
| op=lambda: _num(ak.product_definite(_rat(1, 2), K, _int(1), _int(5)).value), | |
| contract=Returns(1.0 / 32.0, tol=1e-12), | |
| verified_by="Five factors of 1/2 multiply to 2^-5 = 1/32, by the definition of a product.", | |
| xfail=( | |
| "SILENT ERROR: product_definite returns 1. ratuni_poly_to_univ " | |
| "(alkahest-core/src/sum/product.rs:109-144) clears coefficient denominators by " | |
| "multiplying through by their LCM and never returns or reapplies that scale, so the " | |
| "answer is off by c^(hi-lo+1). See temp-alkahest/testing/3.8-silent-error-hunt-2.md." | |
| ), | |
| ), |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@tests/silent_errors/corpus.py` around lines 2326 - 2359, Update the
operations in cases sum_definite_keeps... and product_definite_keeps... to pass
the underlying DerivedResult.value into _num, matching the surrounding
sum/product cases. Preserve all existing case metadata and expressions while
ensuring the xfail cases evaluate the actual numeric result directly.
The fix that stopped `real_roots` silently dropping roots cost 19% on `test_real_roots_deg8` and CI was red on it. Profiling showed the certification ran once on the benchmark polynomial and still cost ~8% of Rust-side runtime — not arithmetic but ~73 mpz malloc/free pairs, because `scaled` cloned coefficients and powers, `reverse_coeffs` cloned again, `taylor_shift_by_1` cloned again, and its O(n^2) inner loop allocated afresh on every one of 36 steps. Three changes, none of which touch what the certification concludes: The certification is skipped where it is provably unnecessary. At that point the search has established an even number of roots in (0, lo) and at least one in (lo, lo+1], so a non-empty (0, lo) forces at least three positive roots — which Descartes' bound rules out whenever sign_var <= 2. The caller already computed sign_var twenty lines earlier and discarded it. Both root-dropping polynomials have three sign variations, so the guard keeps them on the certified path; a Rust test pins that a widened guard would fail. `taylor_shift_by_1`/`taylor_shift_by` are allocation-free in the inner loop, and `sign_variations` no longer allocates. Those run on every VAS frame, not just during certification, which is where most of the win comes from. Measured min-of-N, interleaved, quiet machine, release: the deg8 workload goes 38.76 us at HEAD to 33.19 us, which is also 0.889x the *uncertified* build that was dropping roots. Consistent across degrees 4-16. Correctness re-verified rather than assumed: a reconstructed 2036-polynomial sweep against SymPy has 0 mismatches, and the same sweep against an uncertified build has 155 — so it does bite. Note the pre-fix build looks 2-3x faster on T6, T12 and the cubic only because it returned 6, 12 and 3 roots as 2, 4 and 1; that is not a baseline worth beating. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The residual CodSpeed regression was not the Descartes certification. `x^8 - x - 1` has one sign variation, so the new guard skips certification entirely for the benchmark polynomial — the cost was elsewhere. Attributed by instruction counting rather than wall clock, since CodSpeed runs in simulation mode and the two can disagree: no valgrind available, so a perf_event_open counter (PERF_COUNT_HW_INSTRUCTIONS, exclude_kernel) driven via ctypes around the exact benchmark body, validated linear at 2x work -> 2.0004x count. Bisecting the branch found `exact_rational_root`, added in the *first* round of fixes, costing 142,727 instructions — about 49% of main's entire benchmark. The expression-depth check was ruled out at +1.2% of the build path, which is itself 34k of 393k. The mechanism was `acc *= x; acc += Rational::from((c.clone(), Integer::from(1)))` in the evaluation loop: three mpz GCD canonicalisations and about four allocations per coefficient, ~27 GCDs per degree-8 evaluation, ~8 evaluations per call. Every caller of that evaluation — `exact_rational_root` and `refine_root` — only ever asks for sign and vanishing, never the value. So evaluate the homogeneous form in integers: for x = n/d, H(n,d) = sum c_i n^i d^(deg-i) = p(x)·d^deg. A canonical rug::Rational keeps d > 0, so d^deg > 0, so H vanishes exactly when p(x) does and carries the same sign. Horner with mpz_addmul, no GCD. Control flow is untouched, including round one's deliberate endpoint-root guard. deg8 goes from 1.568x main (as CodSpeed measured) to 0.9975x in instructions and 0.984x in wall clock, improving with degree: 1.133 / 0.998 / 0.911 / 0.845 at deg 4/8/12/16. Correctness was checked for equivalence, not just for passing: the sweep now also asserts the exactness contract (lo == hi for a rational root), and HEAD's and this build's exactness-gap sets are byte-identical with 0 count mismatches. The 160 gaps are pre-existing and deliberate. A new test cross-checks the integer form against exact rational evaluation over 4 polynomials x 51 numerators x 12 denominators. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This was referenced Aug 14, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pre-release hardening for 3.8, which will run unattended multi-day autoresearch loops. Four of these are silent errors that shipped in 3.7 — confident wrong answers with no exception and no verification flag.
Silent errors (shipped in 3.7)
decideproved false theorems and returned certificates that fail their own equation.Wrong exactly when the deciding point had a non-dyadic denominator:
RootIntervaldocuments that an exact rational root is reported aslo == hi,real_rootsdidn't deliver it, so CAD's all-dyadic sample set never tested the root. Bothdecidecases already in the silent-error corpus were dyadic, which is why this survived. 18 wrong verdicts in the first 150 random polynomials before, 0 in 1000 after. The two-variable path had the same gap (escalating only onEq/Ne): 90 wrong of 243 → 0, with no correct answers lost to refusal.Matrix.nullspace()returned basis vectors that are not in the kernel.[[x,0],[0,1]]gave rank 2 and nullity 1 — 2 + 1 = 3 for a two-column matrix. The full-rank gate recognised only a literal non-zero constant, so every non-literal determinant fell into the rank-1 branch: "could not provedet ≠ 0" read as "det = 0", the mirror of therrefdefect. No exotic input required.simplify(0·0⁻¹) = 1— a value the expression cannot take, reachable asdiff(2/(x−x), x). It was four independent rules, including an egglog ruleset that unions0and1into a single e-class, which no rewrite can patch because an e-graph cannot carry theb ≠ 0side condition.Unbounded and uninterruptible searches
limit(sqrt(x²+x) − x, x, +∞)never returned; now1/2in ~1 ms. The hang wastaylor_coefficients(~3× growth per term), not Gruntz — measured, not assumed.wall_msnow binds to ~1.1× instead of 7–12× or never;request_cancelreaches a running engine (integrate/limitrelease the GIL, following the existingsimplify_paridiom).batch_map(parallel=True)ignored budgets entirely and reported the timeout asE-INT-001— a mathematical verdict a loop records as a permanently closed branch. Now propagates an absolute deadline, so N items can't each get a freshwall_ms.run_with_wall_fallbackpoisoned the whole process: one expired candidate left the sticky cancel flag set, and every later call failedE-BUDGET-003forever.Performance
Matrix::det, 9×9 integerpoly_gcdover ℚ[x], degree 128∫cos·sin⁴⁰/(sin¹⁷+sin+1)∫1/(sin⁹+sin+1)detdocumented Bareiss and implemented O(n!) cofactor expansion — 400× slower than SymPy, now 28× faster. The integrate wins come from noticing the Risch rational route spent minutes insidekpoly_gcdcomputing aRootSumthatverify_antiderivativeis structurally guaranteed to reject.A fraction-free
kpoly_gcdreplacement was prototyped and measured 83× worse; the analysis (bit growth is near-intrinsic, and half of every coefficient is a shared denominator costing a 56–100×rug::Rationalcanonicalisation penalty) is in the audit rather than a rushed rewrite.Docs
decidewas documented as complete — as a selling point — in two places. Sphinx documentedMatrix.inv()(the method isinverse()) andM[i, j]subscripting (raisesTypeError), both false before 3.8.TESTING.md's valgrind loop globbed a package name matching zero binaries and passed while checking nothing, and claimed UBSan coverage that doesn't exist.alkahest_core::throughout the docs is a workspace-local alias — external crates needalkahest_cas::.The CHANGELOG now opens with "Silent errors fixed — do results you already computed need rechecking?", separating what shipped in 3.7 from what was introduced and fixed within this cycle.
Verification
cargo fmt·clippy×4 feature sets ·cargo test --all·cargo doc -D warnings·cargo semver-checks(223 pass, no update required) ·ruff·ty(0 errors) ·check_error_codes(190 codes) · certificate ledger ·pytest2519 passed, 0 failed · silent-error gate 176 cases, 0 silent errors.Every headline number here was re-verified independently after the final rebuild. New trap cases were checked against a pre-fix build to confirm they actually fail without the fix, and each ships with a control so the gate can't pass by refusing everything.
Known, documented, not fixed
Stack overflows abort the process on extreme inputs (
latex~16k terms,str~32k,simplifydepth ~8k); symbolicdet/nullspace/eigenvalsremain super-polynomial;MAX_EXPAND_POW_EXP = 4makes rule-based power expansion a silent no-op at exponent ≥ 5;ExprPoolnever reclaims (documented prominently — a long loop needs a fresh pool per iteration).🤖 Generated with Claude Code
Summary by CodeRabbit