SPARQL conformance — measured scores and every named residual#

Factoidal runs the W3C SPARQL test suites from disk, through the F*-extracted parser, algebra and protocol modules, and reports the result per suite. This page states the scores as measured, says what those suites do and do not test, names every residual, and separates what is proved from what is only measured.

Every number below comes from one re-run of every SPARQL suite against the committed bin/linux-x86_64/w3c_runner binary on 2026-07-30, from the repo root, at tree 873aed4. Nothing here is copied from a document. The machine-readable copy is the test-results dashboard and its latest.json; a number here that disagrees with that file is a bug in one of them, not a judgement call.

Parser and algebra spec are verified in F*; the on-disk backend has unverified OCaml-side optimization layers being migrated back to F*.

Sibling pages: OWL 2 conformance · RDF conformance · per-module assurance inventory.

What these suites test, and what they do not#

They test query results. A mf:QueryEvaluationTest gives a query, a dataset and an expected result set; the engine passes when its answer matches. A mf:PositiveSyntaxTest passes when the parser accepts; a negative one when it rejects. That is a behavioural claim about end-to-end output on the fixtures the Working Group wrote.

They do not test conformance to §18. SPARQL 1.1 Query §18 ("Definition of SPARQL") is where the language is actually defined: the translation from the abstract syntax to the SPARQL algebra (§18.2) and the evaluation semantics of each algebra operator (§18.4-18.5). An engine can produce the right answer on all 338 query tests while implementing an algebra that differs from §18 on inputs nobody wrote a fixture for. Suite conformance is evidence about the fixtures; §18 conformance is a claim about all queries, and only a refinement proof against a declarative statement of §18 establishes it. This project does not have that proof today; the section below says exactly what it does have.

They test the protocol in-process, not on the wire. The 53 Protocol and Graph Store tests pass by dispatching each test's HTTP request through the verified protocol modules inside the runner process. Replaying the same suite against a live factoidal-http socket is not automated — the suite manifest sparql11-protocol.yaml records this in its own remaining: block, along with the fact that Graph Store writes over HTTP require the explicit --rw plus delta-log durable mode (the read-only default answers PUT/DELETE with 405 by design).

They test SERVICE against a local table, not a remote endpoint. The service suite's endpoints are resolved through service_endpoint_lookup, an assume val realised as a hashtable the runner populates from each manifest's qt:serviceData declarations (issue #57). The federation logic is exercised; the network is not.

They are not an independent certification. These figures are generated by this repository from the W3C fixtures. Differential testing against other engines is a separate track and has already found real parser bugs (#325).

Scores#

SPARQL 1.1 — 631 pass, 0 fail, 0 skip (out of 631)#

Grouped by the Recommendation each suite belongs to. Every row was measured in one pass of bin/linux-x86_64/w3c_runner with no arguments, which runs all 34 suites.

SPARQL 1.2 — 254 pass, 0 fail, 0 skip (out of 254)#

Measured with bin/linux-x86_64/w3c_runner --sparql12. SPARQL 1.2 is a W3C Working Draft, not a Recommendation; a green row here is progress against a moving target.

The denominators, checked independently#

Every denominator above was re-derived from the mf:entries list of each manifest rather than taken from the runner. They agree exactly: 631 across the 34 SPARQL 1.1 suite directories, 254 across the 10 SPARQL 1.2 ones. No entry is commented out of any SPARQL manifest, so unlike the RDF suites there is no withdrawn-upstream pool sitting outside the denominator. The 34 directories under third_party/testing/w3c/sparql/sparql11/ and the 34 suites w3c_runner --list reports are the same 34 names — no suite is present in the corpus and absent from the run.

The entailment-regime suite, in detail#

All 70 tests are mf:QueryEvaluationTests. Their manifests declare sd:entailmentRegime on the action; the runner picks the strongest regime it implements, in the fixed order OWL-RDF-Based, OWL-Direct, RDFS, RDF, D, RIF. Resolved that way, the 70 split:

Under every one of these regimes except plain simple entailment, blank nodes in the query pattern act as existential variables; that rewrite is F*-side (SPARQL11.Algebra.rewrite_query_bnodes_pattern).

The single D-regime test is d-ent-01, "D-Entailment test to show that neither literals in subject position nor newly introduced surrogate blank nodes are to be returned in query answers". Its query is SELECT ?L WHERE { ?L a xsd:integer } and its expected result is the empty result set. An engine that applies no D-closure returns zero rows trivially, so this test passes for a reason unrelated to D-entailment support. It is the one place in the 70 where a green cell should not be read as a capability.

Disposition vocabulary#

Each residual carries one of five labels, from the completeness ledger's fixed vocabulary (issue #308):

• by-design — the test asks for something outside what this engine claims, citing the suite's own metadata or a written scope decision.
• planned-family — a real gap in a named family of missing behaviour, tracked and intended.
• dependency-blocked — waiting on a capability elsewhere in the engine.
• disputed-fixture — the fixture itself is defective or its expected verdict does not follow; documented per test.
• environment — toolchain or harness, not semantics.

Residual failures#

There are none. Measured 2026-07-30, every SPARQL 1.1 suite and every SPARQL 1.2 suite reports 0 fail and 0 skip. The disposition table that the OWL and RDF pages carry is empty here.

An empty residual table is the point at which a conformance page has to work harder, not less: with nothing failing, the only remaining honesty is about what the green rows do not cover. The two sections below are that.

Harness escapes on the green rows#

The runner reports its own escape branches (issue #316) so that a pass produced by the harness rather than by the engine is visible rather than silent. On the 2026-07-30 run of all 34 SPARQL 1.1 suites, the totals were budget_exceeded:0 gsp_seed:1 no_manifest:0 zero_tests:0 skip:0 unsupported:0 over 631 discovered tests.

• gsp_seed:1, in http-rdf-update. One Graph Store test expects a graph to be in the store before it runs — the manifest names it as operating on an "existing graph" or one "already in store" — and its pre-state was not established by a preceding test in the run. The runner manufactured that pre-state by PUTting a single seed triple, and counts the branch because it can turn a would-be FAIL into a PASS. One test out of 19 in that suite; 18 ran against pre-state a real preceding request created.
• Everything else is zero. No test hit a time budget, no manifest was missing, no suite discovered zero tests, nothing was skipped, and nothing scored unsupported.

By contrast, the RDF 1.1 Semantics suite has ten passes decided without running any entailment check; that is measured and named on the RDF conformance page. Nothing of that shape was found in the SPARQL suites: no SPARQL test type returns Pass before reading its expected result.

What is proved versus what is measured#

The rest of this page is measurement. This section is the part that is not. For the strongest proved statements read end to end in one sitting — parser, expressions, filters, modifiers, results, and streaming, each with its exact domain and honest boundary — see the review kernel; the full theorem registry carries every proved statement (~140 rows).

Three claims are easy to blur together, and the project keeps them apart deliberately (issue #313): a module can be implemented in F*, accepted by the F* verifier, or proved correct against a formalisation of the spec stated independently of the code. The third is rare. The machine-derived, hand-edit-free record of which module is which is the per-module assurance inventory — its oracle is extraction, and it fails downward, so a module is under-credited there rather than over-credited.

⚠️ One caveat on the inventory's numbers, from #328: its theorem-class counts depend on build state, because the oracle asks whether a module's extracted .ml exists on disk and 12 of those files are gitignored. In fresh-clone / CI state the tool reports 30 W3C-refinement theorems; after a local ./build-ocaml.sh extract it reports 0. Every figure quoted below was re-derived on 2026-07-30 in a fresh worktree with no local extract — the same regime that produced the committed artifacts — and matched them exactly. The assume val, admission and --lax counts are pure source scans and never flip; the shipping-function counts quoted here are stable too, because every module named on this page has its extracted .ml tracked in git.

SPARQL11.Algebra today#

Read straight off the inventory (tree fcb83d8; re-derived 2026-07-30 with identical totals):

Zero declarative relations means there is nothing in the module for a refinement theorem to refine to. The nine algorithm-correctness theorems relate shipping functions to each other — lemma_filter_union (filtering distributes over union), lemma_sm_merge_empty_l, lemma_store_search_empty, lemma_eval_bgp_store_empty_fuel, and the three RDF.Store.Columnar.DeltaMerge theorems that tie merge-on-read to apply_entries_ref. Those are real algebraic facts about the implementation. None of them states that the evaluator computes the §18.4 evaluation semantics, because §18.4 is not written down anywhere in the tree as a relation.

The 14 assume vals matter for the same reason. Five of them — eval_expr_ebv, eval_expr_fwd, eval_exists_fwd, eval_subselect_fwd, eval_property_path_fwd — are the evaluator's own mutual-recursion knot, tied on the OCaml side by minimal_regrettable_glue_code_each_with_an_open_issue/62_forward_ref_wiring.sh (issue #62). They are acknowledged gaps under iron rule #3, not allowed realisations: every call the algebra makes through them is assumed rather than verified, and any future theorem about eval_select_query would have to close that knot first. service_endpoint_lookup is issue #57; the rest are hash, Unicode-case and clock primitives.

SPARQL11.Parser (5,308 lines, 269 shipping functions) is merely Tot — zero assume vals, zero admissions, zero lemmas anywhere in the corpus that mention its functions. Its evidence is 94 positive and negative syntax tests in syntax-query, 55 in the update syntax suites, and the 178 SPARQL 1.2 triple-term syntax tests. SPARQL.Protocol (104 shipping functions) is likewise merely Tot, measured by 53 tests.

Landed 2026-07-30 — the refinement vertical#

The two refinement agents that were in flight when the table above was measured have both landed. The table describes SPARQL11.Algebra itself, and it is still accurate: not one line of the shipping module changed. The declarative relations live in a separate, fully-erased companion module, exactly as the simple-entailment pattern prescribes.

Both verify with no admit, no --lax, no --admit_smt_queries and no assume, under z3 4.13.3. The Spec module's whole open list is FStar.List.Tot and RDF.Term — it names no function and no type of the evaluator, so a reader can diff it against the W3C text without the evaluator in view. That independence is mechanically checkable, not a promise.

The fragment proved is named SPARQL-CORE-8 and is stated in the design note. Compatibility, merge, Union, Filter, Project, Minus, Join by the nested loop, Extend/BIND and the degenerate LeftJoin arms are covered. The general LeftJoin arm, eval_bgp_store, and Slice/OrderBy are not.

🔴 The attempt found two live bugs, and neither specification was weakened to make the proof go through. Both non-refinements are machine-checked theorems, and both were then confirmed end to end against bin/linux-x86_64/factoidal:

• #336 (SR-1) — SELECT DISTINCT returns duplicate rows. distinct_solutions compares solution mappings position by position; §18.3 makes a solution mapping a partial function, in which binding order carries no meaning.
• #337 (SR-2) — the hash-join key is finer than the compatibility test it narrows, so the candidate set is not a superset of the matching pairs. OPTIONAL therefore returns a wrong row rather than dropping one. Same root cause as #324, reached from the other end of the tree.

Both live under suites that score 631 pass, 0 fail (sparql11) and 254 pass, 0 fail (sparql12). That is the point of the exercise: a refinement proof is a claim about all queries, and the suites are a claim about the queries in the suites.

Design note: docs/designissues/2026-07-30-sparql-algebra-refinement.md.

The pattern this vertical followed#

RDF simple entailment is the one completed semantic-refinement vertical in this tree, landed 2026-07-29 (design note docs/designissues/2026-07-29-simple-entailment-refinement.md, issue #318). The shipping search RDF.Entailment.Simple.simple_entails carries 17 refinement theorems against relations defined in separate, fully-erased specification modules — soundness, completeness, an iff, a model-theoretic characterisation, blank-node-label independence, and a parser-boundary theorem. Its soundness is conditional (graph_exact on both graphs) and the missing case is itself machine-checked as a counter-example, simple_entails_not_sound_unconditionally, tracked as #324. Details on the RDF conformance page.

That is the shape a SPARQL result would have to take: a declarative §18 algebra written independently of the evaluator, then soundness and completeness of the shipping eval_* functions against it. Nothing smaller changes the claim.

The whole-tree picture#

Across 194 analysed modules the inventory reports 6 with a W3C-refinement theorem, 7 with an internal-refinement theorem, 19 with an algorithm-correctness theorem, 6 pure specification/proof modules, 11 with local lemmas only, and 139 merely Tot. Zero active admissions, zero --lax / --admit_smt_queries regions, 143 active assume val declarations.

So the defensible sentence about SPARQL today is: an F*-implemented SPARQL 1.1 engine, machine-checked for totality, termination and its stated local properties, with 631 pass, 0 fail (out of 631) on the official suites and 254 pass, 0 fail (out of 254) on the SPARQL 1.2 Working Draft suites — and no machine-checked proof that its evaluator implements §18. Those are different claims and this page will not merge them.

Where the numbers live#

• Live scores and history: test-results dashboard.
• Per-module assurance: assurance inventory.
• Per-suite disposition ledger: docs/claude-rules/w3c-completeness-ledger.md.
• Tracking issues: #313 (claim discipline), #62 (the evaluator's forward-reference knot), #57 (SERVICE endpoint resolution), #305 (SPARQL 1.2), #316 (harness escape reporting).
• How the pieces work, with runnable cells: asking questions with SPARQL, mutating and serving data, reaching out to other data.