IBK3 worker and browser SPARQL milestone — 2026-09-01#

Outcome sought#

Make the Shardborough query-worker design executable and visible without claiming that the diagnostic browser ABI already supplies the native store's manifest, Merkle, sidecar, delta, or range-read guarantees.

Tracking issue: https://github.com/danbri/factoidal/issues/637

Landed design boundary#

scanIBK3Predicate(ibk3Hex, predicateIri, blankNodeScope) is a stateless Lean operation. It:

1. decodes hexadecimal input to bytes;
2. runs the complete IndexedBlockWireV3.decode admission path;
3. rejects malformed framing, CRC, row positions, term references, PTD1, or predicate locality;
4. performs a predicate-bound IndexedBlock.scanBound;
5. prefixes blank-node labels with a grammar-safe encoding of the required source/dataset import scope;
6. returns a JSON envelope containing the scope, row count and N-Triples fragment.

It is registered in the same dispatch table used by native and WASM builds. The API deliberately does not parse SPARQL. A coordinator chooses the physical operation; the broader Lean SPARQL runtime combines the returned RDF fragments. "Worker" describes that execution role; the Hub page invokes it in the page's existing WASM runtime and does not create a JavaScript Web Worker.

The scope is shared by all predicate blocks from the same import unit and must differ across unrelated units. Scoping by artifact would be wrong: it would split one source blank node when its description crosses predicate blocks. Leaving labels unscoped would instead coalesce same-spelled document-local nodes when fragments from different inputs are concatenated. Fable identified this boundary during pre-commit review on 2026-09-01.

The current string/hex/N-Triples ABI is a diagnostic bridge for small complete artifacts. Hex decode and source-scope encoding use reverse accumulators rather than repeated append; the scope is capped at 256 UTF-8 bytes. Artifact and output sizes remain unbounded and transport still makes avoidable copies. The operation must not be presented as an internet-facing worker protocol. A production protocol needs authenticated byte buffers or ranges, explicit limits, snapshot/epoch context, typed result buffers, and stable kernel/program/input identities.

The diagnostic response is N-Triples, so it produces a default-graph fragment and cannot preserve named graphs. blankNodeScope is not a GraphId. Dataset workers and future block revisions must carry graph identity separately.

Browser demonstration#

Hub post 51 ships three current IBK3 artifacts generated by the Lean l4block-shard-pack publisher from formal/lean4/Harness/TestData/three-way-subject.ttl:

The page checks each committed SHA-256 identity, calls scanIBK3Predicate three times, joins the N-Triples fragments, and passes the result to queryDataset in the same Lean-derived WASM module. The default three-pattern query returns six solution mappings. Dana's two names and two team memberships produce four mappings, so the demo exercises SPARQL bag multiplicity rather than only distinct subjects.

The user can edit the SPARQL text and render SELECT or ASK results through the accessible result custom elements. CONSTRUCT output is shown as RDF text. The page opts into the Hub's form-first presentation: its implementation remains available through Edit, but the initial reading view leads with the form instead of several screens of JavaScript.

Owner testing found that replacing the join with SELECT * WHERE { ?person ?p ?v . } exposes all 13 decoded rows. The page now makes that exploration a named button and documents both the actual contents of its three predicate blocks and the canonical IBK3/PTD1 byte arrangement.

Native path versus browser path#

The native l4block-id-v3-query host remains the fuller Shardborough execution path. It reads an activated generation, admits manifest-bound artifacts and Merkle ranges, uses SRI2/TLI1/OLI2 access paths, merges durable deltas, and records requested and fetched bytes. Hub post 51 does none of those things; it demonstrates the portable complete-block kernel and composition boundary.

Files in this increment#

• formal/lean4/Wasm/Ops/Block.lean
• formal/lean4/Wasm/Dispatch.lean
• formal/lean4/Wasm/native-smoke.sh
• docs/shardborough-storage-spec.md
• docs/web/hub/51-query-shardborough-blocks-in-browser.md
• docs/web/hub/assets/blocks/shardborough-three-way/
• tests/hub/post51_test.mjs
• npm/factoidal/l4.js, its declarations, package documentation, and package test for the typed helper
• post 46, post 50, and the Hub index for navigation/current-status cleanup
• generated Lean-WASM mirrors after the final build

Verification record#

WASM dependency-closure repair#

The first browser link exposed a real packaging defect rather than a worker defect: Storage/Bytes.lean imported Std.Tactic.BVDecide for its u32 round-trip theorem, and Storage/DeltaLog.lean used bv_decide transitively for the u64 reconstruction. Their generated C consequently referenced proof- tactic initializers which the deliberately narrow runtime build does not ship.

Both round trips now use Lean core UInt/BitVec lemmas to split and rejoin the exact 8-bit and 32-bit slices. This changes no encoder or decoder definition and therefore changes no wire bytes. The scratch-generated C was also checked to contain no Tactic or BVDecide initializer. This is the right boundary: proofs remain checked, while proof automation does not become a runtime dependency of the portable block kernel.

Completed verification:

• lake build l4wasm-cli l4block-shard-pack: passed, 240 jobs;
• Wasm/build-wasm.sh: passed; all documentation and npm mirrors agree on a 4,601,755-byte module with SHA-256 935a3ac5d7f43b5da60e1502b35f796ef9748ded65eece3547410e44371f7122;
• formal/lean4/Wasm/native-smoke.sh: 59 passed, 0 failed;
• the smoke publishes a real current IBK3 artifact before invoking the dispatch operation and separately checks corrupt-byte rejection;
• the four affected Hub/npm test files: 16 passed, 0 failed;
• the full npm suite using a writable temporary cache: 252 passed, 2 skipped, 0 failed;
• full lake build: passed, 891 jobs;
• tools/blockengine-ibk3-persistent-smoke.sh: passed, including the six-row three-property query and update/compaction regressions;
• documentation build: 539 pages written successfully;
• headless macOS Chrome, against the built Pages-shaped site: all three real artifacts loaded, 13 triples decoded, six result rows rendered, no cell or console errors, no horizontal page overflow at 1280 px or 390 px, and all six rows rendered in the mobile card view.

The repository-wide link checker still reports 341 older broken links outside this increment. Post 51 and its three block assets are not among them; that existing site-wide debt is not treated as a pass for the global checker.

Next worker increment#

Specify the first bounded buffer request independently of PostgreSQL and TiKV. It should authenticate an SBM-selected artifact/range before decoding, carry limits and snapshot epoch explicitly, and return binary typed rows plus counters. Only after that contract is executable should it acquire a numbered wire magic or be exposed as a remote service.