GH-5905 Add experimental query algebra equivalence checker - #5948
Open
hmottestad wants to merge 46 commits into
Open
GH-5905 Add experimental query algebra equivalence checker#5948hmottestad wants to merge 46 commits into
hmottestad wants to merge 46 commits into
Conversation
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two executable counterexamples where AlgebraEquivalenceChecker proves a commuted join EQUIVALENT (JOIN_COMMUTATIVE normalization proof) while evaluating both trees against a bundled dataset returns meaningfully different results, and BoundedCounterexampleFinder verifies that same dataset as a witness of non-equivalence: - leftjoin-condition-blind-spot: externalReads(LeftJoin) ignores the condition expression, so a condition reading a sibling-bound variable (may-bind via a Union branch, exposed by the well-designed-left-join path) does not block commutation; the original binds ?c, the commuted tree does not. - extension-overwrite-blind-spot: orderIsObservableAcrossOperands models reads and discards but not re-binding writes, so an Extension that overwrites a sibling-bound variable commutes; the original returns one row, the commuted tree returns none (differs even under ASK). The tests pin the current defective verdicts; flip the EQUIVALENT assertions to NOT_EQUIVALENT once IncomingBindingAnalyzer models condition reads and re-binding writes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
BindingSetAssignment's opaque diagnostic encoding was derived from getSignature(), which embeds the rows' toString(): equal binding sets rendered with different column insertion order produced different canonical encodings while canonical equality (ExactTreeEquality) said the trees were equal, so ProofKernel.verify rejected the checker's own normalization proof (AssertionError) and equal fingerprints hashed into different buckets. StructuralKey now renders VALUES rows through the order-insensitive CanonicalEncoding, with explicit placeholders for unset and non-materialized row sources (a one-shot Iterable must not be consumed by diagnostics). getSignature() itself no longer NPEs on the API-legal unset-rows state. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
RDF4J literal equality compares language tags case-insensitively, but
the canonical encoding wrote the raw tag, so term-equal literals
("a"@en vs "a"@en) encoded differently: SET-mode VALUES deduplication
missed the duplicate and equivalent queries came back UNKNOWN.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
scan() deduplicated visited nodes with a value-equality HashSet, so a structurally equal node whose equals-invisible isVariableScopeChange flag differed was skipped and its correlation sensitivity silently lost; the visited set is now identity-based. duplicateFree(Extension) forwarded to its argument even when an ExtensionElem overwrites an already-bound name, which can collapse distinct rows into duplicates; overwriting extensions now report duplicateFree=false. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two confirmed false-EQUIVALENT soundness holes in the incoming-binding analysis: - externalReads(LeftJoin) never collected the OPTIONAL condition's variables, so a condition reading a sibling-bound may-bind variable (exposed by the well-designed-left-join path) did not block JOIN commutation. Condition reads not guaranteed by the left arg now count as incoming reads. - orderIsObservableAcrossOperands modelled reads and discards but not re-binding writes: an Extension overwriting a name the sibling operand may bind commuted freely although ExtensionIterator clobbers the incoming value. IncomingBindingInfo now carries a rebinds set, collected from ExtensionElem targets and propagated through all combinators, and rebind/may-bind overlap makes order observable. The two pinned counterexamples flip from documenting the defect to asserting NOT_EQUIVALENT with a verified witness; the test class is renamed JsonTupleExprSoundnessRegressionTest accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
isOuterProjection() walked getParentNode() without a boundary, so equivalence verdicts depended on ancestors OUTSIDE the two compared expressions: the same join pair flipped from NOT_EQUIVALENT (detached) to a false EQUIVALENT when both sides were still attached under a live outer Projection, contradicting the module's own evaluation oracle, which always evaluates detached clones. The analysis root (the expression handed to normalize()/externalReads()/ containsRuntimeCorrelation()) is now threaded through the analyzer and the parent walk stops there; canonicalizer-built detached fragments use themselves as the boundary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The filter-into-LeftJoin push rebuilt the LeftJoin with scopeBoundary=false regardless of the node's own flag, so two trees differing only in the LeftJoin's variableScopeChange flag canonicalized identically and were proved EQUIVALENT whenever a relocatable filter sat above them — although the flag steers evaluation (incoming-binding exposure) and every other canonicalization path preserves it. The push now refuses scope-boundary LeftJoins; the sibling union-distribution recursions were already unreachable for boundary nodes via the ordered early return. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Seeded random TupleExpr generator over the checker's supported grammar, a 16-mutator catalog (semantics-preserving and -breaking), scope-safety corpus and legacy-optimizer pair sources, and a differential oracle holding every pair to five invariants: EQUIVALENT verdicts must survive the checker's own BoundedCounterexampleFinder (mandatory because check() short-circuits on the proof path), NOT_EQUIVALENT witnesses must replay stably, check() must not throw, verdicts must be deterministic and order-coherent, and JSON round-trips must preserve tree equality and the verdict. FuzzSmokeTest runs deterministically in every build; FuzzSoakTest (@tag slow) takes equivalence.fuzz.* system properties, shrinks failures and persists reproducible artifacts under target/equivalence-fuzz/. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the equivalence differential fuzzer: ExtensionIterator installs a null-binding placeholder when a BIND errors, which reads as unbound via getValue(), so BindingSetAssignmentQueryEvaluationStep's compatibility check correctly concludes a VALUES row may bind the name — but ArrayBindingSet.getDirectAddBinding asserted the slot was never written and crashed any assertion-enabled run (plain builds already performed the overwrite, which matches SPARQL join semantics). The assert now tolerates the placeholder. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the equivalence differential fuzzer: ProjectionElemList implements VariableScopeChange, but the JSON format serializes the element list as a bare array, so a set flag was silently dropped by parse(write(tree)) and the round-tripped tree was no longer ExactTreeEquality-equal. Projection now carries an additive projectionElementsScopeChange field; MultiProjection, which has no representation for a per-list flag, fails the write loudly instead of round-tripping to a semantically different tree. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ession manifest CheckerCompletenessGuardTest regenerates a fixed 40-pair set (seed 0xC0FFEE) and compares every verdict against fuzz/completeness-ledger.csv — a soundness fix that legitimately degrades a proof to UNKNOWN now forces a visible one-line ledger diff instead of slipping through; aggregate floors catch outright coverage collapse. Each run rewrites target/completeness-ledger-bootstrap.csv for easy re-pinning. JsonTupleExprFuzzRegressionTest is manifest-driven: promoted fuzz artifacts (first entry: the shrunk VALUES-over-null-binding crash pair) are re-checked on every build for both robustness and their pinned verdict. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the equivalence differential fuzzer: when incoming bindings overlap the VALUES names, the compatibility-checked path only created a result once it saw a row NAME, so the empty mapping was dropped entirely — while an equal row that carried its UNDEF columns as name-with-null (a parser-built ListBindingSet) passed through. Two equal trees evaluated to different results depending on which representation their rows used. Empty and all-UNDEF rows now join as the identity mapping on every path, and raw rows returned by the no-incoming-bindings fast path are stripped of declared-but-UNDEF columns so the representation difference can never leak downstream. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A declared-but-UNDEF column stored as a name with a null value binds nothing, so it must not count toward a VALUES node's possible or assured binding names — otherwise equal rows that merely represent UNDEF differently derive different names. BindingSetAssignment and the equivalence module's BindingAnalyzer now ignore null-valued columns. SemanticsValidator additionally rejects a BindingSetAssignment whose rows were never set: evaluating such a node fails at precompile time, so no algebraic proof about it can be checked against runtime behaviour (the fuzzer produced EQUIVALENT verdicts for trees whose runtime behaviour was an exception). Completeness ledger re-pinned for the one intentional NOT_EQUIVALENT-to-UNKNOWN move this causes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the equivalence differential fuzzer: a Var carrying a value but NOT flagged constant is a real variable at runtime — the statement pattern step uses the value as a constraint AND binds the name into the result row (only isConstant() vars are skipped). The binding analyzers filtered on hasValue(), so such variables vanished from may/must-bind domains: MINUS_DISJOINT_DOMAINS erased a MINUS right side whose rows actually shared a runtime binding name with the left side, proving trees EQUIVALENT that a witness dataset distinguishes. BindingAnalyzer and the incoming-binding fallback collector now discriminate on isConstant(); ExpressionVariables stays on hasValue() because value expressions evaluate the embedded value, not the binding. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The license header URL was missing the /org/ path segment, which fails the copyright-check CI job (scripts/checkCopyrightPresent.sh requires the exact http://www.eclipse.org/org/documents/edl-v10.php line). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Self-review follow-ups to the declared-vs-derived binding-name split: ArrayBindingBasedQueryEvaluationContext wrote the derived names back through setBindingNames, which now sets the DECLARED header — so merely precompiling a query silently dropped all-UNDEF declared columns from the model (the write-back was an interning optimization; getIndex has an equals fallback, so only the interning read remains). The SPARQL and SPIN renderers now prefer the declared header so a column that is UNDEF in every row is not dropped from rendered output. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The .agent working document belongs to a different workstream and has no place in the algebra-equivalence PR. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Self-review follow-ups: FuzzSoakTest runs in the pr-verify slow-tests job, so its default seed is now fixed (a nanoTime default would fail unrelated PRs nondeterministically; pass equivalence.fuzz.seed for exploration); the optimizer pair source uses insertion order instead of per-JVM-salted Map.of iteration so seed-pinned repro commands replay the same pair schedule; the smoke test writes artifacts per seed and fails loudly if the time budget truncates the battery; the soak asserts the corpus actually produced pairs and reports truncation; the vacuous NOT_EQUIVALENT floor is gone; the shrinker documents its same-invariant-not-same-defect limitation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
BindingSetAssignment.getBindingNames() now derives names from the
actual rows, so the zero-row 'VALUES (?a) {}' placeholders in SHACL's
bulked validation queries report an empty name set and all three
injection sites silently skipped setBindingSets — transactional
validation then ran against an empty VALUES and under-reported
violations that span transactions (e.g. a maxCount violation whose
prior value was committed earlier). The injection sites now match on
getDeclaredBindingNames(), and the experimental
PreprocessedQuerySerializer prefers the declared header so zero-row or
all-UNDEF columns are not dropped from rendered output. The new
BulkValuesInjectionTest pins the cross-transaction bulk path end to
end (red before this fix).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The per-query configuration read is now memoized on the raw property strings (re-parsed only when a property actually changes) and never throws: a malformed org.eclipse.rdf4j.query.scopeSafety.* value logs one warning per distinct bad tuple and disables the features, instead of failing every query in the JVM from inside optimize(). read(Function) stays strict for direct callers and tests. Also introduces the shadowStrict property (default false) consumed by the next commit's shadow-containment work. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
SHADOW is an observation mode, so it must never change what the user gets back: candidate-plan exceptions (at optimization AND evaluation time) and result mismatches are now recorded as telemetry and the already-materialized legacy rows are returned; the new shadowStrict property (default false) restores fail-fast behaviour for CI/canary runs. A candidate that returns more rows than the fully-enumerated legacy result is recorded as a MISMATCH (it is provable), not a row limit. Sequence comparisons are only strict when the root's order is actually guaranteed (an Order reached through order-preserving operators) — a nested Order/Slice no longer forces bogus sequence mismatches — and a Slice with no backing Order is skipped as NONDETERMINISTIC since two valid plans may legitimately return different row subsets. Sequence divergences with agreeing multisets count as SHADOW_ORDER_DIVERGENCE instead of mismatches. AUDIT remains fail-fast by design and both contracts are now documented on ScopeSafetyMode. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The mode-dispatch bridge was copy-pasted across seven optimizers in two modules with three diverging shapes; the divergence included an ENFORCE+non-QueryRoot edge where FilterOptimizer/ProjectionRemoval fell through to their scope-UNSAFE legacy pass. ContextAwareQueryOptimizer now carries a single static dispatch with an explicit per-optimizer EnforcePolicy (SKIP for join reordering/normalization and the LMDB pair, REPLACE for the filter/projection scope-safe rewrites — never falling through on fragments, now pinned by a test — and RUN_LEGACY for the scope-safe union scope-change relaxation). AUDIT keeps the eager refresh (it IS the audit mechanism); SHADOW's legacy leg no longer pays an eager ScopeAnalysis rebuild per optimizer that nothing consumed. OptimizationSession.afterLegacyOptimizer drops its unused Class parameter; ScopeSafeRewritePass.projections() gains the convergence cap the other drivers already had; and the TransactionalTreeEditor move/factory API, unused by every rewrite, is deleted (rollback keeps the install-reversal core). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The parser now sets the subquery flag accurately (nested sub-selects true, the top-level projection false) and optimizers introduce flag-false projections as deliberately TRANSPARENT correlated nodes, so TupleExprs.containsSubquery must keep honouring the flag — a positional rule was prototyped and refuted by the spec-verified scope-safety fixtures (q03 lost a row in ENFORCE because an internal transparent projection was suddenly treated as an isolation boundary). The residual obligation is documented and pinned instead: code that embeds a parsed top-level projection as a join operand is turning it into a subquery and must call setSubquery(true) to get isolation semantics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The rdf4j-queryalgebra-json package is now @experimental like its sibling equivalence module, so japicmp does not semver-lock the new API at its first release. TupleExprJsonParser's JsonNode entry point gains the decoder-level depth guard the stream entry points already had via StreamReadConstraints — a hostile-depth prebuilt JsonNode now fails with a TupleExprJsonParseException instead of a StackOverflowError. The equivalence README documents the scope-safety modes, including the ENFORCE optimization loss (join reordering and normalization are skipped) and SHADOW's lenient-by-default containment. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
BindingSetAssignment.clone() carries the derived binding-name caches (they depend solely on the shared immutable row reference), removing an O(#rows) rebuild on every per-execution clone of a VALUES query. SHADOW sampling decides BEFORE cloning the tree — at low rates the whole-tree clone was built and discarded for almost every query — and uses ThreadLocalRandom instead of a structural hash that was both badly skewed and deterministic per query. The ProofKernel's re-derivation of freshly computed proofs (which doubled the cost of every successful check) moves behind CheckOptions.deepProofVerification, default off; the differential fuzzer keeps it on. The three scope-safe rewrite passes now share one fixpoint driver instead of three diverging copies. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
SemanticFingerprint/Fingerprinter/FingerprintIndex, SemanticAnalyzer(Impl), SemanticSummary and CardinalityBounds were unreachable from check(), and BindingShapeOracle, SemanticLivenessAnalyzer and RewriteRuleId had no production callers. Their tests pinned only the deleted code. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The seed now records only frames, regions, environments, symbol name/frame, origins and their occurrence symbols. Fingerprint, physical names, symbol visibility, occurrence roles/ordinals and the whole boundary/export/allowed-input section had no production consumer; dropping them also removes their per-parse recording cost in QueryScopeSeedRecorder. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The BFS in TupleExprs.containsSubquery returned false as soon as it dequeued a Join, ending the scan before any queued Union siblings were examined. Join and LeftJoin evaluation use this helper to decide whether the right-hand side needs subquery scope isolation, so the decision — and the query results — depended on Union branch order: LeftJoin(x, Union( subselect, Join(..))) isolated the subselect while the commuted LeftJoin(x, Union(Join(..), subselect)) pushed bindings into it. Found by the differential fuzzer (soak seed 71601, pair seed 73613): the checker correctly proved a union-commute pair EQUIVALENT but the runtime returned different bags. The bug predates this branch. A Join operand stays opaque (its own evaluation owns the projections inside it), but the scan now continues with the remaining siblings. The shrunk pair is pinned in the fuzz-regressions manifest. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the differential fuzzer (soak seed 71603, pair seed 73681): commuting a Join whose operand contained a Distinct changed the result multiset. Pushing a sibling's bindings into a Distinct/Reduced argument that can produce solutions with differing domains collapses solutions that differ only in an unbound variable, and a Slice truncates filtered instead of unfiltered solutions — neither matches bottom-up semantics. Join and LeftJoin evaluation now isolate operands flagged by the new TupleExprs.containsResultSetModifier. Uniform-domain Distinct/Reduced (every possible name assuredly bound, e.g. the parser's path? encoding, whose ZeroLengthPath depends on correlation) stay on the push-down path, which is injective and therefore stable for them. Isolation is only correct if the isolation join is: HashJoinIteration hashed on may-bind names, silently dropping rows whose join attribute was unbound on one side, and its merge never checked value equality on shared non-attribute names. It now hashes on assured-on-both-sides names and verifies full SPARQL compatibility per bucket row. A conditional LeftJoin on the isolation path used to drop its condition entirely (also for pre-existing subquery right-hand sides); the new ScopedLeftJoinIterator materializes the right-hand side once and applies compatibility plus the condition per left-hand row. The shrunk pair is pinned as fuzz-regressions/distinct-pushdown-join-commute, and the manifest test now re-runs the full differential oracle on every pinned pair under all three profiles. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
CartesianJoinExplainAnalyzer treated a transparent projection's whole element list as a mandatory-region atom. Since the parser started marking the top-level projection subquery=false (making it transparent to the region walk), that atom mentioned every output variable and spuriously connected all patterns under any top-level SELECT, so real Cartesian products lost their explain annotation (QueryPlanRetrievalTest.testExplainAnnotationsEmitDisconnectedJoinTypeTextAndJson). A projection element only correlates variables when it renames (?name AS ?alias); identity elements now contribute no region atom. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
RDF4J eagerly precompiles both operands and the condition of a LeftJoin before either input is evaluated, so eliding one can hide a deterministic preparation failure. An invalid constant regex in a LeftJoin condition fails even when the right input is empty, which means folding LeftJoin(x, EmptySet, badCondition) to x turns a runtime error into a result. Demote LEFT_JOIN_EMPTY_LEFT, LEFT_JOIN_EMPTY_RIGHT, LEFT_JOIN_UNIT_RIGHT and MINUS_EMPTY_LEFT to specification-only rules: the Lean constructors gain an explicit notRuntime premise, and CertifiedRuleRegistry and Rdf4jCanonicalizer enforce the same restriction on the Java side. The rules remain theorem-backed for SPARQL_1_1, SPARQL_1_2 and BOTH_1_1_AND_1_2. The rule/profile matrix moves from 347/677 to 323/701 theorem/inapplicable cells. Adds JsonTupleExprSoundnessRegressionTest# eagerConditionCompilationBlocksLeftJoinEmptyRightFold and CertificateReplayNormalizerTest# rejectsRuntimeRulesThatElideEagerlyPrecompiledSubtrees as regressions. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The previous commit blocked the four elision rules under RDF4J_RUNTIME by
adding a notRuntime premise to the Lean constructors. That fixed the
symptom from outside the model: referenceEval still defined
leftJoin left .empty condition = referenceEval left
for every target, discarding the condition, so the model kept asserting an
equivalence that is false of RDF4J. The restriction was a policy bolted on
top of a semantics that could not express the defect, because
ReferenceEnvironment.evalCondition returns a total Bool and preparation
failure is unrepresentable.
Give the model the missing phase. ReferenceEnvironment gains
conditionPrepares, and conditionPrepared applies it for RDF4J_RUNTIME only:
that target compiles a condition once before either input is evaluated,
while the specification targets evaluate per solution and cannot fail
preparation. The elision equations now propagate what they discard, so the
four theorems carry ConditionPrepares and RuntimeOperandTotal premises
rather than holding vacuously.
Because the premises are real, they can also be discharged. An absent
condition has nothing to precompile and an EmptySet/SingletonSet operand
cannot fail, so checkStep decides elisionFree syntactically and the rules
stay available at runtime exactly when the elision is observationally free.
This recovers the completeness the target gate gave up: LeftJoin(x, EmptySet)
with no condition is EQUIVALENT again under RDF4J_RUNTIME, where the
previous commit returned UNKNOWN. The matrix returns to 347/677, now backed
by discharged premises instead of a universally quantified falsehood.
CertifiedRuleRegistry mirrors the premise as permitsConditionElision and
permitsOperandElision; Rdf4jCanonicalizer and LocalCertificateReplayer
consult them where the rule is applied. The same guard closes the
previously unprotected Filter-over-EmptySet fold, which discarded a
condition with no rule recorded.
The finite oracle can now witness a preparation failure, so the sweep can
refute a bad elision certificate rather than being blind to the class.
Adds reject-runtime-condition-elision and valid-runtime-elision-free
fixtures covering both directions.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
GitHub issue resolved: #5905
Briefly describe the changes proposed in this PR:
This PR adds an experimental
rdf4j-queryalgebra-equivalencecore module for conservatively checking whether two native RDF4J query-algebra trees are equivalent before accepting an optimizer rewrite.Validation:
python3 .codex/skills/mvnf/scripts/mvnf.py core/queryalgebra/equivalence --retain-logs— 56 tests, 0 failures, 0 errors-Pquick clean install— BUILD SUCCESSPR Author Checklist (see the contributor guidelines for more details):
mvn process-resourcesto format from the command line)