Persisted query ladder — 2026-09-02#

Owner goal, 2026-09-02, verbatim: "Performant standards-compliant formally verifiable e2e RDF/SPARQL MVP, showing snappy searches against increasingly large dataset converted to Shardborough formed rdf indexed data."

This note is the measurement record for that goal on the persisted path (l4block-shard-pack → l4block-shard-activate → l4block-id-v3-query, see skills/shardborough-storage). Every number is a single cold run on one laptop (Apple M-series, macOS, formal/lean4 native build) unless a column says otherwise; timings are wall-clock for the whole process, including manifest read, Merkle verification, decoding and result printing. Rows are counted by the CLI.

Rung 2: gene.ttl, 888,949 triples#

Query workload#

The six competitive-bench queries (docs/test-results/competitive-bench.json) plus a bounded scan and an object-bound lookup.

The "before" column was measured while a WASM build competed for CPU; the two columns are therefore comparable only where the open mode changed (q3, q6). Every query returns the same row count and the same preview rows in both columns. q3's bytes read fell from 24.9 MB to 0.24 MB logical; q6's from 24.9 MB to 2.7 MB.

Reference points from the same store: the plain join ?s P1057 ?o1 . ?s P688 ?o2 returns 9,117 rows in 2.4 s through the subject-join path (4 shards, 3.0 MB read); ?s P1057 ?o1 alone returns 25,058 rows in 0.54 s.

Diagnoses#

• q3, q6: planning, not engine. Both fall to the full-manifest path. For q3 the harness had no selective path for an unbound predicate, although every block carries a TLI1 term index and SRI2 subject postings that the join path already uses. For q6 the constant-predicate collector (ShardManifest.nativeConstantPredicates?) refused OPTIONAL, so the planner read all 13 blocks (24.9 MB) and evaluated over 888,949 triples; the same two predicates as a plain join read 4 shards.
• q1, and every full-manifest read: Merkle verification in pure Lean. The profile of q3 before the fix is dominated by BlockMerkle.nextLevel, Crypto.sha256, processBlocks256 and sha256CompressBlock: SHA-256 in pure Lean at roughly 5 MB/s over 25 MB, before any decoding. HACL*'s SHA-256 is already vendored and linked for the Ed25519 family (third_party/hacl/src/Hacl_Hash_SHA2.c, native and WASM), so a host-side hasher realised by HACL* is available under the crypto policy; the pure Lean sha256 stays the specification because build-time #guards run in the interpreter, which cannot call an extern.
• The evaluator's physical plan has no OPTIONAL arm. Once q6 reads only its two predicates, the LeftJoin still runs on the reference evaluator over the fragment. A native LeftJoin arm with its refinement proof is the next engine-side step (L4Factoidal/SPARQL/StoreDataset.lean).

Rung 2.5: the whole life-science extract, 1,290,077 triples#

All twelve Turtle files of examples/wikidata/subsets/lifesci-kgx/data/ concatenated (31,603,120 bytes), through the same path, measured 22:25 with nothing else running.

The selective paths scale with the number of blocks probed (q3: 13 to 52 blocks, 0.12 s to 0.20 s), not with the triple count. The two costs that scale with bytes are activation (one full verification and index recomputation per generation, 45 s for 51 MB) and the whole-store count.

Rung 3: the UK Parliament dump, 3,143,406 triples#

third_party/data/ukparliament/ukparliament-rdf-2019-07-27.trig, 346,861,556 bytes, 5,325,830 lines, one unlabelled graph block (the TriG default graph). Converted to Turtle by dropping the two brace lines; packed with the same command as the rungs above. The content is dominated by e-petition signature counts (four predicates hold 2.2 million of the 3.1 million triples); the procedure-browser vocabulary the sample queries use is almost absent (29 :name triples, 405 typed entities), so the sample queries answer zero or few rows, correctly: the F* engine's recorded bench shows no rows for the same queries.

Measurement caveat for this rung (2026-09-03): on the 16 GB MacBook the same binary on the same store gave 30 s and 985 s in two alternating runs (1,138,990 triples), and one run of the full-store activation took 1,017 s after a run of 152 s. The stalls coincide with memory pressure (the reference parse of the 134 MB region alone reaches 5.39 GB resident; the list-based decoders hold about sixteen bytes per artifact byte) and are not reproducible with the byte-array decoders, which were stable at 104 s. Report such numbers only from alternating runs on an idle machine, and say which runs were discarded and why.

What this rung teaches:

• Answers stay correct at 3 million triples; the selective paths stay at tens of milliseconds even when a query names eight predicates.
• Pack and activation were the bottleneck, and the cause was not the predicate or block count (the first reading of this rung said it was; the slice ladder below disproved it). It was the statement scanner reversing the accumulated candidate at every line end, which the 134 MB polygon statement group turned into hours. After the fix pack is 254 s and activation 165 s for the same generation (the section "Where the 6,134 s went" below has the method).
• The constant-predicate collector refused BIND and property paths, so two queries read all 309 blocks (356 MB) and evaluated on the reference path. Since commit cf36c8e90 (2026-09-03) BIND with a backend-local expression and sequence, alternative and inverse paths over constant IRIs are collectable; *, ?, + and negated property sets are not (the first two pair every node with itself, so restricting the dataset drops answers). A BIND + OPTIONAL + GROUP BY query over predicates the store holds: 20 rows both ways, 309 shards / 47 s → 2 shards / under 1 s. Found while doing it: EXISTS in HAVING, ORDER BY or a projection was evaluated against the opened shards only — https://github.com/danbri/factoidal/issues/638.

Findings from the first, failed attempt (2026-09-02, late):

• The first pack failed after 867 s with Turtle parse error at 202943268: expected object. Cause: the TriG-to-Turtle conversion used BSD awk, which stopped at about 203 MB on the 3.9 MB polygon line and truncated the file; the error position is the cut-off last statement. Not a parser defect. The conversion was redone in Python and the full pack repeated.
• The reference Turtle parser (parseTurtle, behind l4factoidal parse and the WASM datasetOpen Turtle path) is quadratic: 2,514 triples 0.38 s, 5,012 triples 1.51 s, 10,012 triples 6.16 s. Two token readers compute their fuel as the length of the remaining character list once per token (readTurtleString, readNumericLiteral); the whitespace skipper had the same pattern removed earlier. The packer's chunked path bounds each chunk, which is why packing still runs at about 4 MB/s. FIXED 2026-09-02 late: the literal loops take the constant literalFuel (2^32) and the old per-token forms are kept as readTurtleStringSpec / readNumericLiteralSpec; Syntax/TurtleFuelTheorems.lean proves the loops fuel-independent above the remaining length and the constant-fuel readers equal to the specification forms for every input shorter than 2^32 characters (axioms: propext, Classical.choice, Quot.sound only). After: 5,019 lines (2,734 triples) 0.30 s, 10,019 lines 0.37 s, 20,019 lines 0.74 s — linear. Gates: W3C RDF 1.1 Turtle 313 pass and TriG 356 pass, RDF 1.2 Turtle syntax 67 / eval 29, TriG syntax 35 / eval 25, all 0 fail; native-smoke 63 pass (out of 63).
• The dump has a 3,875,112-character line (a geosparql:wktLiteral polygon) and 223 sibling polygon literals in one statement group. That group alone parses in 1.4 s and packs correctly, but the pack takes 57 s for 224 triples: multi-megabyte literals go through the term codec, the PTD1 pages, the TLI1 keys and the Merkle leaves several times each. A per-term size limit or a separate large-literal store is a design question for the corpus ladder, not a correctness problem.
• l4block-shard-pack on an empty input produced an empty generation that activated (recorded in the shardborough-storage skill).

Where the 6,134 s went (2026-09-02, late): the statement scanner#

Method. A size ladder of UK Parliament slices with no literal over 10 KB (the first such literal is at line 1,702,684 of 5,360,986), each packed and activated on an idle machine with the Turtle-fixed binary:

Linear in triples, and the block count (18 to 47) does not show. The gene store on the same idle machine: 888,949 triples, 13 blocks, pack 11.5 s, activate 13.4 s (13 µs per triple). So neither predicate count nor block count explains the full dump's 1,950 µs per triple.

The remaining candidate was the region of large literals: 345 lines over 100 KB, 105 MB of the 341 MB file, all inside lines 1,702,684 to 1,706,891. Cut as one 134 MB Turtle file (4,211 lines, 3,560 triples), it packed in 334 s with the committed binary — 100 s more than the whole linear ladder above put together.

Cause. Syntax/TurtleStatementScan.lean decides at every line end in normal mode whether the current candidate is a no-dot directive (PREFIX, BASE, VERSION), and did so by reversing the whole accumulated candidate (dropWs currentRev.reverse) to read its first word. That is O(lines × characters) per statement group: the polygon group has 4,211 lines and 134 MB, about 280 G list steps.

Fix. StatementScan now carries head, the first seven characters after leading whitespace, maintained per character by pushHead; the directive test reads it. The old form is kept as directiveHeadSpec, and Syntax/TurtleStatementScanTheorems.lean proves head = directiveHeadSpec currentRev for every run of the scanner from init (axioms: propext, Classical.choice, Quot.sound only).

After, same region: pack 81 s, activate 109 s with the three-pass activation and 62 s with the decode-once activation of commit 389b47f1a (both measured with another pack running on the machine). The whole dump: pack 254 s (was 6,134 s), activation 165 s idle (was 4,554 s). The remaining 81 s is the reference parse (31 s for this file: 19 s user, 9 s system reading 134 MB as a character list) plus the term codec, PTD1 pages, TLI1 keys and Merkle leaves over 105 MB of literal bytes; the activate is four full decodes per block (ShardActivate.verify* each decode the primary again) over the same bytes. Those are the next two items for this rung, with the large-literal policy question above.

Stage profile after the fixes (2026-09-03, temporary IO.monoMsNow timers, two runs each; the 134 MB region, 3,560 triples, 28 blocks):

On the 370,355-triple slice without large literals the shares are similar but the absolute index-sidecar cost is 9 s, so both largest stages track literal bytes, not triple count. The two lines that do the work: IBK3 encode? converts the PTD1 dictionary ByteArray to a List UInt8 and back with ++ (IndexedBlockWireV3.lean, dictionary.data.toList then byteArrayOfList); TLI1 entriesOf builds a List UInt8 key per term and sorts with a cons-cell comparator (TermLocalIndex.lean, lessBytes). Both were dispatched as bounded changes with byte-identity and theorem gates. Outcome: the IBK3 encoder change (ce7db9def) saved the predicted 20 s. The TLI1 change (ByteArray keys, mergeSort with entriesOf_eq_spec) saved 2 to 3 s, because a sampler run (/usr/bin/sample) showed the 46 s index-sidecar stage is 17 s primary IBK3 decode plus 16 s TermLocalIndexWire.decode? (which re-serializes every term to check its stored key and walks the file as a List UInt8); entriesOf was 2.2 s and its sort 0.1 s. The code-reading attribution to the sort was wrong (anti-pattern 28: state the method next to the result; a sampler sees what a reading cannot). Next bounded item: the two decoders over ByteArray indices with the list forms kept as the specification. The reference parser on the same file: 22.9 s user, 21.7 s system, 5.39 GB maximum resident set (the List Char representation; design record section 2.4).

Gates for the scanner change: all 378 artifacts of the 320,019-line slice byte-identical between the old and new scanner; W3C RDF 1.1 Turtle 313 and TriG 356, RDF 1.2 Turtle 67 + 29 and TriG 35 + 25, all 0 fail; native-smoke 63 pass (out of 63); lake build 922 jobs. The scanner is used only by Harness/PredicateShardPack.lean, so the WASM mirrors are unchanged.

Status#

• Planner fixes for q3 and q6: landed (commit 82d2f530e; the "after" column above). The worker that measured them also found, through tools/w3c-persisted-census.sh, that FILTER NOT EXISTS answered zero rows in the WASM and CLI query path since the morning's backend routing change; fixed the same day with pins in native-smoke.sh, StoreDataset.lean and tests/hub/l4_exists_regression_test.mjs. Census after the fix: 535 executed, 0 refused (out of 535 eligible), the recorded 2026-09-01 numbers.

• HACL* SHA-256 hasher for the host verification path: landed. The pure Lean sha256 stays the specification; the host passes a HACL*-backed Hasher into the Merkle and artifact functions, and lake exe l4vc-probe checks the two agree on the FIPS vectors, the block boundaries and a 1 MiB buffer (13 pass, 0 fail), as a required CI step. Measured on the gene store, single runs, hasher the only difference:

  Operation	Pure Lean hasher	HACL* hasher
  COUNT(*) over the whole store (full-manifest read)	7.49 s	3.94 s
  l4block-shard-activate of the 25 MB generation	52.95 s	13.81 s
  l4block-shard-pack chromosome.ttl	1.01 s	0.72 s

  Block bytes are unchanged (the chromosome block keeps sha256 01484578…). What remains in a full read is decoding and index building, not hashing.

• LeftJoin physical arm with refinement proof: landed. SPARQL.hashLeftJoin buckets the right side once on the shared always-bound variables, and hashLeftJoin_eq_leftJoin (SPARQL/IndexedEvalRefinement.lean) proves it equal to the nested-loop leftJoin as a list, rows and order; the reference evaluator's OPTIONAL arm and a new backend arm (conditions in Expr.backendLocal) both use it, and the backend join arm now uses hashJoin (licensed by hashJoin_eq_join). Guards compare the backend runner with the reference on extending, unmatched and rejected OPTIONALs.

Milestone table, 2026-09-02 evening#

Single cold runs on the same store, everything of the day landed; a WASM build was competing for CPU during these runs, so the quiet numbers are a little lower (q1 measures 3.94 s quiet).

Every row count and preview is unchanged from the morning. What backs the numbers: the codecs' round-trip theorems (spec section 10.1), the hash join and hash LeftJoin equalities, the backend-arm theorems, the encoder admission equal to the decoder's, and the HACL* SHA-256 differential probe in CI. What remains outside a theorem: the planner's choice of blocks (argued in docstrings, checked by the census and the row-count comparisons) and the extern hasher's agreement with the specification (checked by the probe).

• Rung 3 (UK Parliament TriG, 347 MB, named graphs): blocked on the quad-aware layout (spec section 10, gate 4); the packer reads Turtle only.