Cache recursive plans and bound page prefetch

[theronic]

What changed

• cache immutable recursive traversal plans by permission root inside the selected schema-proof generation
• share schema-only compilation across principals while keeping grants, visited graph state, continuations, and completed answers query-scoped
• evict plans with the rest of derived schema state
• adapt recursive backend scan batches to the Relay window: 16 datoms through page size 32, 32 through 256, and 64 for larger pages/counts
• expose fetched-stream and stream-fill counters so prefetch regressions are deterministic rather than timing-only
• document the exact cache granularity and the absence of SpiceDB-style graph-subproblem caching
• extend the Dafny operation-count model with at-most-once plan compilation and bounded page-sensitive stream batches

Root cause

Recursive queries reused schema path and routing classification caches, but rebuilt traversal rules, forward-consumer indexes, and reverse rule indexes on every cache miss or cache-disabled request. That repeated work depends only on immutable schema, not graph data or the principal.

Separately, every recursive graph stream prefetched 64 datoms even for a 20-result UI page. The engine consumed only 93 datoms for the Explorer page but could realize substantially more backend data. Page-sensitive batches preserve 64-datom amortization for large scans while removing most small-page over-read.

Safety boundary

A plan is keyed inside a backend/source/schema-proof generation. It contains only schema-derived rules and indexes. Authorization answers and request-local traversal state are never shared. Raw or arbitrary DB evaluation without a trusted schema proof still compiles per request.

The formal release gate intentionally remains withheld: the complete public Clojure/CLJS engine is not generated from the proof kernel. SchemaPlanCost.dfy proves deterministic operation-count properties and is paired with runtime counters; it does not claim wall-clock verification or full-engine refinement.

Performance

DataScript browser benchmark on the Explorer recursive 10k-server seed, 20-result page, 20 samples after warmup:

• release/v8.0 before: 4.549 ms mean, 4.460 ms p50
• this PR: 3.255 ms mean, 3.200 ms p50
• improvement: 28.4% mean, 28.3% p50
• completed-cache hit: 0.146 ms mean

The schema-plan cache is a safe cross-principal compilation network effect. The measured small-page gain comes primarily from bounded prefetch. Large page scans retain the 64-datom batch.

Validation

• JVM: 397 tests, 13,369 assertions, 0 failures/errors
• DataScript CLJS: 103 tests, 1,388 assertions, 0 failures/errors
• heavy pagination/load suite: 9 tests, 3,403 assertions, 0 failures/errors
• generated Java differential boundary: 18 tests, 7,143 assertions, 0 failures/errors in a fresh nREPL
• Dafny: every source report verified with 0 errors; SchemaPlanCost.dfy has 14 verified obligations
• generated Java, JavaScript, and browser bundles built successfully
• Dafny formatting and git diff checks pass

Explorer consumer: theronic/eacl-explorer#3

[theronic]

Benchmark update after the page-sensitive recursive stream batching (DataScript browser, Explorer recursive 10k-server seed, 20-result page, 20 measured samples after warmup):

build	uncached mean	uncached p50	cached mean
release/v8.0 before	4.549 ms	4.460 ms	0.152 ms
PR #100	3.255 ms	3.200 ms	0.146 ms

That is a 28.4% mean and 28.3% p50 uncached improvement. The full JVM, CLJS, generated-boundary, Dafny, and heavy pagination suites remain green; exact counts are in the PR description.