Skip to content

Fix #439 and #447: t2s rank gates throw; no real claims for a negative radicand - #474

Open
petlenz wants to merge 3 commits into
mainfrom
fix-439-447-domain-gates
Open

petlenz wants to merge 3 commits into
mainfrom
fix-439-447-domain-gates

Conversation

@petlenz

@petlenz petlenz commented Sep 17, 2026

Copy link
Copy Markdown
Member

Closes #439.
Closes #447.

#439 — t2s invariants reject a wrong-rank operand. trace, norm and det gated rank with assert, so an NDEBUG build constructed a malformed node that reached the evaluator. They now throw invalid_expression_error through the same validate_rank helper the tensor side uses (#438), and dot's hand-written check moved onto it too.

Side benefit: the rules added in #427 rely on trace's rank precondition — try_trace_identity assumes a rank-2 identity, try_trace_outer_product assumes rank-1 operands. A real throw makes those preconditions hold in release builds as well; verified that trace(I4) and trace(otimes(X,X)) (rank 4) both throw.

#447 — no real-domain claims for a negative radicand. sqrt claimed nonnegative + real for any argument, and pow claimed real whenever base and exponent were real, though both are NaN on a provably negative operand. Now suppressed when the base is provably negative and the exponent is provably fractional — including a negated fractional exponent (pow(n, -1/2)) and a double spelling (0.5), both verified by probe.

Deliberate scope: an unknown-sign operand keeps the claims, since unassumed symbols are real by default in this propagator. Tightening that would mean sqrt(x) on an unassumed x claims nothing, a broader policy change than this issue.

Negative controls:

Full suite 2407/2407 (gcc-14 Debug) plus a Release build; clang-format clean.

Authoring note: the agent that wrote these changes was interrupted by a rate limit mid-review. Its in-progress probe (the negated-exponent hole it suspected, and the #427 preconditions) was completed — both came back clean — the probe file removed, and the verification above run against the finished branch.

trace, norm and det gated rank with an assert, so NDEBUG built a malformed
node that reached the evaluator. They now throw invalid_expression_error
through the same helper the tensor side uses, which also makes the rank
preconditions the trace rules rely on hold in release builds.

Signed-off-by: petlenz <peterlenz89.pl@gmail.com>
sqrt claimed nonnegative and real for any argument, and a fractional power
claimed real whenever base and exponent were real, though both are NaN on a
provably negative operand. An unknown-sign operand keeps the claims, since
unassumed symbols are real by default here.

Signed-off-by: petlenz <peterlenz89.pl@gmail.com>
…ative

Composed negativity escaped the radicand guard: -(x*x)-1 concluded only
nonpositive, so sqrt of it still claimed nonnegative and real though the
value is NaN for every real x. A sum now concludes a strict sign when every
term shares it weakly and at least one holds it strictly.

Signed-off-by: petlenz <peterlenz89.pl@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

1 participant