Adopt stable-discovery enumeration: sealed plans, width-one reducer, stable cursors - #116
Merged
Merged
Conversation
added 30 commits
August 12, 2026 20:01
…idence Rewrite the adopt-stable-discovery-enumeration planning artifacts to the verified simplified design: one generic reducer over sealed plans, result uniqueness by construction, width-one-only physical execution with the concurrency seam preserved, two cache artifacts, three-outcome adapter result classification, consistency-aware continuation, scalar checkpoint ordinals carrying the lookahead segment, and a re-sequenced delivery plan (local gates, route, delete, then remote performance qualification). Task 2.1: archive the durable exploration evidence (accepted prototype, Dafny/TLA models, contracts, audits, benchmark protocols, probe project) into tracked exploration/stable-discovery/, excluding regenerable run state and dependency caches per its ARCHIVE.md.
Tasks 2.2, 2.3, 2.5 and the CLJ half of 2.4: a deterministic baseline capture harness (eacl.baseline.capture, eacl.baseline.perf) freezes the current engines as differential oracles through the public DataScript API with answer caching disabled. Seven fixtures cover direct, union-overlap, deep-arrow, recursive chain, recursive star, mutual recursion with a data cycle, pure data cycles, and a broad 8-way union with a late-productive principal. Snapshots record authoritative denotations, counts, point checks, pagination invariants, cursor idempotence/fork behavior, typed cancellation and timeout validation, and stale-basis continuation outcomes; legacy page order is recorded as informational only. The perf snapshot records warm-repeat medians plus authoritative first-execution logical scan counts (60 scans across 4 permission paths for a 20-item dense first page on the 2k-server fixture). eacl.baseline.baseline-test verifies snapshots reproduce (77 assertions). Remaining in 2.4: CLJS latency/allocation and containerized MinIO/JDBC/ DynamoDB-local operation baselines, documented as open items in exploration/baselines/README.md.
Tasks 3.1, 3.2, 3.5: port the retained-scope formal models from the evidence archive into formal/stable-discovery/ — 41 Dafny leaves (506 obligations), the AtomicAttempt and ProgressCheckpoint TLC families with their mutation configs, the randomized refinement campaign (18,000 checks, 22 mutation controls), and the five retained source bridges — with a self-checking fast gate (verify-fast.sh) that enforces model/config/bridge manifests, the TLA assumption-boundary fingerprint, the exact obligation count, and a 10 s wall ceiling (~7 s observed, green). Parked with the future concurrency change (archive-only): ReducerReadAhead, DescriptorCoalescing, ServiceLifecycle, ReadableWorkIndex, and WeightedResponseLease (30 obligations) plus the physical-scheduler bridge. The rejected candidate's untracked formal models are quarantined pending deletion at task 9.2; dispositions recorded in the tree README.
Tasks 4.1-4.4 and the machine core of 5.1: eacl.engine.sealed-plan compiles the reachable four-kind rule program fail-closed directly from the adapter's schema-definition operations (independent of the legacy compiler), assigns dense canonical ordinals, certifies the static 0/1 shortest-remaining-storage-read rank with an untrusted generator and a linear trusted checker, orders every alternative vector by (rank, ordinal), and folds the plan, order contract, and admission-key granularity into one composite fingerprint. eacl.engine.stable-reducer executes sealed plans in both directions on one unified width-one machine: right-edge stack, exact per-kind admission (merge points keyed by node + entity, scans by ordinal + binding excluding the resume bound), logical release hard-fixed at one value per transition, bounded evictable chunk buffers with the authoritative resume bound carried on the residual work item, and single root emission keyed by the emitted entity in each direction. Differential gates (eacl.engine.stable-reducer-test, 99 assertions): denotation equality with the frozen current-engine baselines on all seven fixtures forward and reverse; exact result-sequence invariance across physical chunk widths 1/2/7/64 and buffer retention policies; target-prefix stability; and the permission-alias-cycle counterexample for node-qualified interior admission keys. The dense 20-result first page costs 17 adapter commands versus the legacy merge's 60 on the same fixture.
…-demand seam Tasks 5.1-5.4: admission identities become a specialized immutable per-kind key type with a cached hash on the JVM (vectors on CLJS); the admitted set and result vector become request-owned transients held linearly by the run loop and frozen at finish; admission, command, and transition limits are checked before their transition commits and fail with a typed uncommitted :eacl.reducer/limit-exceeded error; scans are equality-complete read-demand descriptors realized through one injectable fetch seam (the direct width-one adapter path today, the concurrency extension point later); and finish enforces the always-on structural invariants fail-closed. Behavior is unchanged: the full differential suite (99 assertions — frozen-baseline denotations both directions, width/retention order invariance, prefix stability, alias-cycle counterexample) stays green.
CLJ halves of tasks 3.3, 3.4, and 5.5 in eacl.engine.stable-discovery-gate-test (60 assertions): - An independent naive-fixpoint oracle — sharing only the adapter's schema-definition reads with the compiler and nothing with the reducer's plan/order/admission machinery — reproduces every fixture denotation in both directions, establishing soundness, completeness on exhaustion, and termination through cycles against an evaluation-independent authority. - The sealed-plan bridge proves semantic rules, ordinals, and ranks are invariant under schema clause order, that certified rank distances equal an independent Bellman-Ford oracle, and that the linear certificate checker kills understated-distance, missing-witness, and oversized-hop mutants. - Six engine mutation controls are killed: entity-only interior admission keys (alias fixture), per-rule root keys, unreversed successor push order, host-ordered alternative buckets, fetched-end resume bounds (under forced refetch), and eager whole-chunk release on the overlap geometry — where the gate also pins the accepted one-value order (subtree discovery precedes later siblings). Neighboring suites remain green (176 assertions across the reducer differential and frozen-baseline suites).
Section 6: eacl.engine.stable-page executes stable-discovery pages over the generic reducer. Public cursors are bounded domain-separated HMAC edge tokens binding format and order-ABI versions, the composite plan fingerprint, source lifecycle, exact basis, anchor, direction, fixed page size, boundary ordinal and external identity, and optional expiry; navigation mode is request input. Continuation is a latest-only in-process checkpoint per execution identity — history-free reducer state plus the undelivered lookahead segment and constant-size boundary identity, replaced only on a strictly greater scalar transition ordinal, with entry and weight caps and overweight drop — or governed deterministic replay that validates the boundary before any page publishes. Basis changes reject typed (stale-cursor, or cursor-consistency-conflict under a fresher consistency demand), and replay budget failures surface as the distinct resource-exhaustion error. The reducer gains history-free checkpoint extraction and resume with delivered/discovered separation. Gates (eacl.engine.stable-page-test, 56 assertions): page composition equals one-shot traversal at four page sizes with and without checkpoints in both directions; cursor fork/idempotence; checkpoint and replay agreement; lookahead survival with the missing-segment mutant killed; checkpoint nonregression and overweight drop; backward windows with start clamping; tamper/page-size/key rejection; and the typed exhaustion cliff. Full new-engine battery: 292 assertions green. The page-size-one composition failure caught a real undercount in the continuation arithmetic (pending values double-counted against the resume target); fixed and locked by the gate.
…nd routes Section 7: eacl.engine.physical provides three-outcome read classification with cause codes (complete, classified failure, or cancelled — realization inside the boundary discards partial output atomically), retry of the exact descriptor under the original absolute deadline with separate attempt accounting, the service-edge admission bulkhead with slot-hold and the replay ledger, cooperative cancellation cut points from the execution contract, the closed topology capability record with conservative defaults and width pinned to one, and per-layer cost telemetry. The Datomic and Datahike select-exact paths now classify instead of swallowing Throwable to nil: genuine absence maps to the contractual unavailable signal, interrupts classify as cancelled, and every other fault propagates as a typed retryable failure. (The two backend files also carry their pre-existing one-line traversal-execution and identity-contract declarations.) Section 8: eacl.engine.stable-route implements the resource-anchored point check with first-admission early exit and exact counts by reducer exhaustion with explicit truncation, both verified against the frozen baselines. Gates (eacl.engine.physical-route-test, 61 assertions): the remaining in-scope mutation control (atomic partial-output discard) is killed; retry/terminal/deadline semantics; admission and replay quotas; cancellation through the page path with no publication; capability validation; point checks and counts against every frozen sample; and the binding CLJ local perf gate (median within legacy warm + 0.25 ms, allocation within the legacy full-compute envelope, no linear scaling with unvisited branches). Full new-engine battery: 353 assertions green.
Task 9.4: docs/stable-discovery-engine.md summarizes the published order ABI, cursor trust boundary and rejection classes, three-outcome failure semantics, cache artifacts and per-layer telemetry, and topology qualification requirements, referencing the normative specs.
Keep the adapter SPI additions the stable-discovery engine and the committed backend declarations depend on: the adapter version bump, the conservative and strict-sequential traversal-execution profiles, profile normalization/validation, and the DataScript snapshot adapter's profile declaration. Effective concurrency width remains one everywhere.
Task 9.1: lookup-resources, lookup-subjects, can?, count-resources, and count-subjects now execute on the sealed-plan stable engine on every backend. Pages return :stable-edge cursors (one-based ordinals, composite plan fingerprint) through the existing authenticated relay envelope; backward navigation runs the bounded before-window, and :last without a cursor returns the final window of the exhausted sequence. Point checks are anchored reverse traversals with first-admission early exit; counts exhaust the reducer with explicit truncation. Public :recursive-traversal-limits map onto the reducer budgets and surface under the established :eacl.recursive-traversal/limit-exceeded key with :limit-kind preserved; the public :evaluation modes remain accepted and are equivalent by construction on the exact engine. Sealed plans are cached per concrete snapshot identity + basis + root (a cross-store cache-key collision was caught by the cross-engine differential during the flip and is bound in that suite). The frozen-baseline suite becomes the cross-engine differential: the new engine reproduces the previous engines' denotations, counts, and point checks through the public API on every fixture; legacy-order and old-engine-mechanics assertions retire in favor of the stable-engine gates (three tests updated to the new order ABI, the old routing and denotation-cache certifications removed with their machinery). Also removes the dirty experimental tree (the rejected byte-stable candidate's uncommitted diffs across the engine, kernels, relay, continuation, and formal manifests; its untracked scheduler, governor, ABI switch, and formal models), keeping the traversal-execution SPI groundwork the stable engine uses. Verification: 3,838 assertions green across the Datomic, DataScript, relay, baseline, and stable-engine suites; the 506-obligation formal gate passes at ~7 s.
The stable-engine gate suites and baseline harness exercise the DataScript backend, but lived on the shared eacl test path that every isolated module job loads — failing namespace resolution on the datomic and datahike classpaths. They now live in the eacl-datascript module, snapshot paths resolve from either the repo root or a module working directory, and the CLJS test runner drops its references to the removed routing suite.
Retarget the minimized counterexample corpus, execution-contract evidence, and smoke suite rosters from the deleted old-engine regression suites to the stable-engine gates that certify the equivalent properties (anchored point checks, exhaustion counts, oracle equality, alias admission keys, checkpoint continuation, token rejection, fingerprint identity); every one of the 67 minimized bugs replays green against its new closing evidence (3,479 assertions). Restore the count-pagination-keys definition lost in the entry-point splice, declare deliver-page ahead of its edge-page use (a fresh-classpath load failure the REPL masked), regenerate the public source closure for the new engine namespaces, and drop the archived exploration probe logs from Git — they are regenerable run output whose figures are quoted in the audit documents.
Operator-reported: repeated pagination replayed every page. Three independent faults compounded: - The stable engine only accepted a raw atom as its checkpoint store and silently discarded the client's scoped continuation context, so no checkpoint ever survived a request. checkpoint-put!/checkpoint-hit now adopt the context (fn-map) storage with the same latest-only, nonregressing semantics, and report :continuation-hits. - The sealed-plan cache was keyed on JVM object identity, missing on every fresh Datomic snapshot. It now keys on the adapter's declared source identity (backend, scope, lifecycle, revision, root); the baseline fixture that shared one lifecycle across distinct stores violated the source-identity contract and is fixed instead. - The Datomic client's internal-page validator did not recognize :stable-edge cursors, so the answer cache never remembered any stable page. cursor-result gains the :stable-edge case, restoring same-basis memoization and cross-basis generation-proof lifting. Also restored on the routed engine: execution enforcement (deadline and cancellation cut-points from the request contract were inert), the bare-:last complete-evaluation guard (now scoped to recursive plans via a Kahn cycle check sealed into the plan), per-run observer stats under the public counter names, and a portable token clock for the CLJS build. New gates: continuation_reuse_test pins checkpoint reuse, answer-cache hits for repeated pages and counts, plan reuse across snapshot re-wraps, and distinct fixture lifecycles.
The aggregate CI job runs suites the isolated-module pattern misses; those still asserted the retired engine's counters and cache layering. - Plan compilation sharing is asserted by counting seal-plan calls, and the synthetic test adapters mint per-construction lifecycles like real stores (a shared constant would alias plan-cache identities). - Old work envelopes (:derived-grants and friends) are re-bound to the stable engine's admission accounting: page work stays page-proportional in every evaluation mode, continuation resumes are page-bounded rather than zero-cost (EACL-FORMAL-002's invariant is no closure recompute), and the exhaustion tail on final pages is schema-constant. - Cancellation, deadline, and public-client timeout gates are ported to the stable execution path (:stage :reducer-transition); the retired op-count suite that hosted them is deleted. - The half-retracted-ghost contract is updated: the anchored reverse check fails closed on the missing reverse half while forward enumeration still exposes the orphan until the auditor repairs it. - The local perf gate binds its deterministic command and allocation budgets everywhere; sub-millisecond wall-clock medians are bound loosely on shared or loaded hosts and precisely by the benchmark protocol on reference hardware.
The operator's dev transactor and its million-entity test database run 1.0.7705; the older 1.0.7622 peer cannot read that database's schema level.
Operator-reported on the million-server database: a 24k-result exhaustive count failed :max-queued-work because the public limits were mapped onto the wrong reducer budgets. The public contract is explicit: :max-queued-work bounds instantaneous queue depth, :max-advanced-datoms bounds consumed projection values. - The reducer gains :max-stack (staged depth check at admission) and :max-values (whole-chunk rejection before integration), both atomic like the existing limits. - The public mapping becomes :max-derived-grants -> admissions, :max-advanced-datoms -> consumed values, :max-queued-work -> stack depth. Cumulative transition and command counts stay internal runaway ceilings, scaled with the authorized public work so raising the public limits actually authorizes it (a one-million-result exhaustive count takes more than the fixed four-million-transition default). Gates: a deep-chain count under a tight :max-queued-work must succeed (the reported failure shape), and a tiny :max-advanced-datoms must fail typed with the public :limit-kind. Verified on the demo: the million-server exhaustive count completes in 23s cold, 2.4ms cached; first pages stay page-proportional at 14ms.
- Limit failures surface exactly {:eacl/error :limit-kind :limit} with
the caller's numeric ceiling; reducer budget keys and internal
counters never leak.
- A well-formed authenticated boundary that replay cannot validate
surfaces as a clean :eacl.pagination/stale-cursor (the basis no longer
reproduces the edge) instead of :eacl.page/invalid-cursor with internal
ordinal diagnostics.
- The cross-runtime recursive page vectors and the acyclic differential
smoke gate now pin the stable first-discovery order and the stable
engine's public work counters; the retired per-request acyclic
authorities they asserted are gone with the engine they governed.
The generated-boundary smoke battery passes locally: 50 tests, 15,638
assertions.
Task 9.2: the unreachable machinery kept through the routing flip is gone — the recursive forward/reverse page engines, the certified-acyclic route with its lazy merge-sort enumeration (the mutually recursive traversal cluster static analysis cannot flag), the generated continuation restoration layer, the evaluation router, and the dead acyclic instrumentation branch. v8 drops from 4,956 to 2,690 lines with zero remaining unused-var warnings. eacl.lazy-merge-sort moves to test scope (the corpus already declared it test-only; its remaining consumers are legacy-order test oracles). Test probes of deleted internals are retired with them, and EACL-FORMAL-036's closing evidence re-points at the stable checkpoint-reuse gate, which pins the same continuation-cache-participation property the original bug was about. Verified after the cut: the CI-equivalent battery (623 tests, 26,020 assertions), the generated-boundary smoke battery (49 tests, 15,632 assertions), and the CLJS bundle, all green.
…rage Completing the dead-path removal: the schema-cache analysis half (traversal classification, SCC component plans, the recursive-plan cache) is gone — recursion classification lives on the sealed plan, and the retained permission-path derivation continues to feed the relationship dependency sets that drive answer-cache invalidation. - :relation-populated? leaves the adapter contract: only the retired router probed it. All three backends drop the implementation, the certification harness drops the obligation, and the dispatch evidence re-pins at 57 call sites over 19 operations. - The verified-authority cutover suite now requires the generated decision authority the stable design actually routes through — consistency selection, answer-cache decisions, cursor continuation, and relationship paging — determined empirically. The retired traversal-authority coverage set and the dead-counter benchmark suites it drove are gone. - The Datomic client's cursor-continuation decision now routes through the client's configured kernel like every other generated decision; reading the global selection at request time was the one seam that bypassed per-client kernel selection (and the cutover counter). Verified: CI-equivalent battery 25,983 assertions; verified-authority heavy and nonbenchmark suites both pass with full four-operation coverage on all three backends (36,188 assertions).
added 8 commits
August 14, 2026 20:06
The JVM cutover suite already requires exactly the four generated decisions the stable-discovery design still routes through; the CLJS runner kept demanding the ten retired portable traversal authorities and failed its gate with every one of them unexercised. Mirror the JVM roster. Verified locally: 159 tests, 4,573 assertions, zero gate failures, all four required operations observed.
The gate still observed the retired engines: it bound the inert acyclic work stats, required recursive stats to stay empty, asserted the analysis router's acyclic-routing markers, and gated envelopes in merge-advance/backend-scan vocabulary. Every deftest now observes the stable engine's cumulative run deltas (:derived-grants, :advanced-datoms, :queued-work, :continuation-hits) and the manifest records deterministic stable-counter envelopes from today's observations plus headroom. The benchmark client opts into explicit traversal limits the way deployments do, because the overlapping account/team/vpc fixture paths make exact acceptance counts consume more values than the production guardrail defaults admit. Correctness pins are unchanged: exact deduplicated counts, page exactness, one continuation hit per resumed page, and demand-bounded recursion. The matched-v7 latency gate mechanics are untouched; it reports :not-applicable everywhere today because the recorded host class no longer exists, and tasks.md now records the honest latency picture (pages several times faster than v7, uncached exhaustive counts several times slower pending the width>1 execution change). Verified locally exactly as CI runs it: 7 tests, 84 assertions, zero failures, work counters identical across repeated runs.
A restart step's readiness probe was a bare TCP accept, which the retiring JVM's still-open listener can satisfy in the seconds between SIGTERM and socket teardown. The step then reported success before the replacement JVM had bound the port, and the next gate died on a connection-refused eval with no output (observed once on the routing-certificate resource gate after roughly six prior clean passes). Every restart now waits for the old listener to release the port before starting the replacement, and readiness requires an actual nREPL evaluation round-trip rather than a TCP accept.
…cs into main Every implemented change is archived under openspec/changes/archive with today's date; only adopt-stable-discovery-enumeration stays active. Delta specs were folded chronologically so MODIFIED/REMOVED targets existed when applied. The three v7-era Datomic-only cache designs (add-intelligent, add-consistency-aware, harden-v7-4) were archived without folding: their whole premise was replaced by the v8 chain and one never merged (PR #80). Hand merges where the mechanical fold was refused: modular-backend-workspace 'Shared backend contract' and 'Upgrade documentation' (upgrade renamed the DataScript scenario to cover Datahike; publish's text is kept and the three still-true upgrade scenarios are retained), 'Graph-independent coherence adapter contract' and backend-native-revision-consistency 'Backend capability honesty' (remove-unknown replaces the exact-current-only and unknown-authority scenarios). Requirements contradicted by already-archived newer changes are pruned from main (causal tokens/anchors/journal, explicit coherence authority and proof modes, content-proof cache validity, graph-order retraction bookkeeping, single-flight result join, the reverted derived-digest cache key) and the stale six-function SPI requirement is replaced by the shipped adapter operation contract. Requirements contradicted by the still-active stable-discovery change are declared as REMOVED deltas on that change so its archive folds correctly. The three archived changes with residual open tasks carry a note pointing at where each residue is tracked.
…ease-assurance gate Sweep of definitions with no reference anywhere in src, tests, formal bridges, build scripts or the demo repositories (clj-kondo analysis plus grep), verified by the CI-equivalent battery on a fresh JVM (621 tests, 25,976 assertions, 0 failures) and the DataScript CLJS suite (193 tests, 7,311 assertions): - eacl.engine.v8: the inert acyclic observation vars (*acyclic-route?* was never bound, so *acyclic-work-stats*/add-acyclic-work! never ran), *inactive-recursive-cycle-guards*, *count-stats* (bound, never read), the retired recursive-cursor-version/recursive-order-abi, find-relation-def, schema-version-stamp, and permission-schema-components with its Kosaraju helpers; the Datomic client and eacl.relay drop the :lookup-eid and :recursive-logical cursor kinds nothing has minted since the routing. - eacl.datomic.impl.indexed / impl / db: dead façade wrappers, the *count-stats* bindings, resets of cache keys that no longer exist, relation-populated?, relationship-relation-id, affected-relation-ids. - eacl.subproblem-cache: metric writers of the retired tiers and the two lookup helpers that were declared closure roots with no callers (roots list updated, ledger regenerated). - eacl.formal.production-kernel: dead acyclic/merge bridge functions and nine unused generated-class imports; the reflection mutant detector no longer looks for the two type hints those functions carried. - eacl.spicedb.parser REPL helpers and their pprint require; eacl.engine.relationships/after-cursor?; DataScript/Datahike max-entid, find-relation-def, build-schema-catalog, avet-range, calc-set-deltas aliases, schema-change-attrs; the empty eacl.impl.spicedb stub; unused requires and destructured bindings flagged by clj-kondo. - formal/stable-discovery: the source_refinement_bridge bound to eacl.engine.v8 vars removed by the 9.2 excision and made verify-fast.sh fail with a NullPointerException after its Dafny/TLC stages; the gate's escape-hatch scan used rg and silently skipped when rg was absent. The bridge is removed, the scan uses grep, and the gate is green again (506 obligations, all mutants killed, 6 s). engine/all-permission-nodes stays: it is the only dispatch site of the required :all-permission-nodes adapter operation and the dispatch closure ledger requires one.
…nt contract Rewrites, against the source, the statements that presented the interim v8 acyclic/merge/indexed engines, their cursors and options as current: - README: stable first-discovery order instead of Datomic-eid/"acyclic vs recursive" order, result-edge cursors instead of per-path frontiers, reducer-exhausting counts instead of 16,384-eid frontier pages, eacl_z4_ token examples (eacl_z3_ is rejected), the Datomic-only page-token TTL qualified, cache layers as they exist. - AGENTS.md: the dev/restart-backend! sequence (no such namespace), the CI-equivalent test battery form, the module bench paths, the source-closure regeneration rule; .rules link to clojure-rules.md. - docs/stable-discovery-engine.md: the public envelopes and :eacl.pagination/* keys instead of the standalone eacl_sd1. token and :eacl.page/* keys; failure semantics and topology qualification now say which physical components the routed path installs (only the cut-point). - docs/cache.md and docs/v8-subproblem-cache.md: the live tiers (answer, identity projection, sealed plan, latest checkpoint, visited page) instead of relationship projections and completed denotations. - docs/formal-verification.md, formal/README.md, trusted-boundary.md, production-decision-inventory.md, temporal-model.md, final-assurance-audit.md, integration-spike.md, formal-verification-corrections.md: the generated kernel is authoritative for four decisions and the CLJC stable engine for enumeration; retired Dafny leaves labelled as such pending the task 9.2 cut; stale ledger counts replaced by the ledger itself; complete-logical-page and cloudafrica/eacl references fixed; the decision inventory names the sealed-plan/reducer/page decisions. - docs/release-notes-v8.0.md: six-function SPI, :coherence-authority, denotation reuse, per-relation generation vector, cursor payload v10, route-specific order, routing/merge dispatch and scan waves corrected. - Adapter-boundary, modules-and-upgrade, module READMEs, PORTING.md: populated-relation checks, cursor frontier identity, SCC/fixed-point wording removed; safe_retraction.clj listed. - formal/stable-discovery/README.md: quarantine list of files that no longer exist, task-status sentences, bridge count. - docs/adr and docs/plans gain READMEs marking them historical; the stray "007 ... copy.md" is renamed, ADR 008/009 headers fixed, the 2026-08-07 exploration prompt moved from adr/ to plans/; the v6-vs-v8 benchmark and the v7 arrow bug-fix notes labelled historical (and the benchmark's :live-results option corrected to :remember-answers); docs/index.md links the engine doc and the reports.
Bugs, formal-versus-implementation verdicts, specification and backend discrepancies, dead-code inventory, and optimizations found while auditing core/ at ac3cbac: the exhaustion-target cap on exact counts, point checks and bare :last (reproduced), the standalone stable-page checkpoint key that omits the basis, the unwired section-7 physical components, the Datomic expand-permission-tree codec bypass, Datahike temporal-snapshot identity, the noHistory stamp on the exact path, the broken release-assurance gate, error-shape drift, and the optimizations (schema-generation plan cache, leaf existence probes for can?, dependency-equal checkpoint keys, backward page replay, count materialization) with the soundness argument for each. Records what this branch archived, pruned, corrected and removed.
…s, codec-aware Datomic adapter, temporal Datahike identity, exact fallback on unreadable stamps
Each fix carries a regression test; the CI-equivalent battery on a fresh
JVM (627 tests, 26,009 assertions, 0 failures), the DataScript CLJS suite
(193 tests, 7,311 assertions) and the stable-discovery release-assurance
gate (506 obligations) are green.
- Exhaustive runs are unbounded. `stable-reducer/exhaustion-target` is
positive infinity and is the target of every exhaustive route (exact
counts, anchored point checks, bare :last windows), so a run ends only at
an empty stack or a typed :max-admissions/:max-values failure — never at
the retired 1,000,000-result cap that silently truncated counts and
point checks once the public limits authorized more work
(physical_route_test/exhaustive-runs-are-unbounded-test drives 1,000,001
results through both directions).
- The standalone stable-page API keys checkpoints on the whole execution
binding, basis included, so a checkpoint recorded at one basis is never
resumed by a token minted at another
(stable_page_test/checkpoint-identity-includes-the-basis-test).
- The Datomic client passes :object-eid-fn to its adapter, so
:object-id->internal resolves external ids through the client's
:object-id->lookup-ref/:object-id->ident codec; expand-permission-tree
was the one operation handing the adapter an external id and it resolved
a hardwired [:eacl/id id] instead — an absent topology for codecs whose
ids differ from :eacl/id (config_test/expand-permission-tree-uses-the-client-id-codec-test).
- The Datahike adapter reads configuration through Datahike's IDB/-config
protocol, so temporal (AsOfDB) snapshots report their origin's store
identity, attribute representation, writer and history capabilities
instead of nil (the exact fallback previously minted a different snapshot
identity and lost :fully-consistent); the published store identity is
bounded to {:backend :id} so jdbc/s3 connection configuration never
reaches snapshot ids, cache bases or cursor digests; :read-failed no
longer counts as absence
(consistency_v3_test/temporal-fallback-adapter-keeps-its-source-identity-test).
- The Datomic exact-cursor fallback no longer depends on reading the
:db/noHistory relation stamp through d/as-of: when the generated decision
reports divergence purely because the exact snapshot's dependency proof
was unreadable while its native revision and execution identity are the
cursor's own, the continuation is :exact by identity; readable stamps
that differ still diverge and another revision or source is never
rescued (consistency_v3_test/exact-fallback-tolerates-unreadable-historical-stamps-test).
- The reducer's schedule admits each work-id once per successor batch and
skips nil items, refining StableReducer.Admit literally
(stable_reducer_test/schedule-admits-each-work-id-once-per-batch-test);
the replay ledger dissocs keys at zero; the answer-cache semantic keys
carry the public order ABI; the missing-relation write error is typed
:eacl/unknown-relation-or-permission on all three backends and
:eacl.basis/selection-failure carries :type.
The report records each item's status; the section-7 physical wiring, the
unstamped-Datomic write guard, and the DataScript/Datahike create
serialization and delete batching are recorded as design decisions rather
than repaired.
…onize the error shapes Relationship writes validate their schema names before any endpoint resolves, with the read side's typed taxonomy (eacl.schema.errors/validate-relationship-write!, called by both clients): unknown definition -> :eacl/unknown-definition; unknown relation, or a subject type the relation does not declare -> :eacl/unknown-relation-or-permission (the latter with :reason :subject-type-not-declared). The backends' own "Missing Relation" throws carry the same category as a fallback. Schema writes: reference-validation failures are :eacl.schema/invalid-reference (with the :errors vector), unsupported features are :eacl.schema/unsupported-feature, and every already-typed parser error also carries :eacl/error. validate-schema-references now rejects a relation whose subject type is not a defined definition (SpiceDB rejects `relation reader: nobody`) whenever the schema carries its definition list, i.e. on every write-schema!; Datomic's private copy of the validator is replaced by the shared one. Page requests: out-of-range :first/:last are :eacl.pagination/invalid-page-size (with :size/:max); both directions, both bounds, a bound without its direction, :cursor/:limit and list keys on a count are :eacl.pagination/invalid-page-request; a nil bound keeps :eacl.pagination/invalid-cursor. Harmonized additively across backends: :eacl/unknown-object, :eacl/relationship-conflict, :eacl.schema/concurrent-write (Datomic also reports :expected-generation/:actual-generation/:backend-error) and :eacl.schema/relation-in-use carry :eacl/error equal to :type; the Datomic client's freshness errors use :reason :freshness-timeout/:head-behind/ :sync-failed and carry :requested-order-hint/:observed-order-hint beside their :requested-t/:observed-t. Also: the eacl-datomic release config pins com.datomic/peer 1.0.7705 like the module (the published POM declared 1.0.7622); the README's write-relationships! update shape, per-backend delete-object! semantics and SpiceDB-differences section are corrected; tx-schema-version-guard documents the supported unstamped v7-compatibility regime (a fail-closed variant was tried and reverted: schema_basis_test deliberately writes on an unstamped database). Tests: schema_error_contract_test/relationship-writes-share-the-schema-taxonomy-test and schema-and-page-request-errors-are-typed-test. Battery 629 tests / 26,047 assertions / 0 failures; CLJS 193 / 7,311 / 0.
Section 7 of adopt-stable-discovery-enumeration delivered the three-outcome
read classification, retry, service-edge admission and topology capability
record as library components; the routed public path installed only the
execution cut-point (audit item 2.3). This installs them:
- Every routed adapter read (point checks, lookups, counts) runs through
classified-fetch-fn + retrying-fetch-fn (eacl.engine.v8/stable-fetch-fn):
a foreign adapter failure is classified :retryable and retried up to three
times for the same descriptor under the request's original absolute
deadline, then surfaces as :eacl.scan/failure with :classification and
:cause-class and the original exception as its cause. Typed EACL errors
(contract violations, limits, deadlines, cancellation) pass through the
boundary unwrapped and unretried (physical/typed-eacl-error?), so the
pinned public error contracts are unchanged. Attempts are reported as
:adapter-attempts in the traversal work stats.
- A :service-admission client option ({:max-concurrent :max-replays
:max-replays-per-key}, validated by physical/normalize-service-admission)
installs the bulkhead around routed enumerations (slots held for the full
synchronous call chain, :eacl.service/admission-rejected) and the replay
ledger, keyed by continuation identity, around checkpoint-miss replays,
backward runs and last windows (:eacl.service/replay-rejected). Both
clients bind engine/*service-admission* per request; an omitted option
installs no bulkhead. The ledger dissocs keys at zero.
- Both clients derive the adapter's closed topology capability record from
its declared execution profile plus the engine's read boundary
(physical/adapter-topology-capabilities) and fail closed at construction
with :eacl.topology/unqualified when it does not certify stable discovery
(physical/require-qualified-topology!); the three bundled adapters declare
the strict sequential profile and qualify.
Tests: physical_route_test routed-reads-are-classified-and-retried-test,
service-admission-bounds-routed-enumerations-test,
topology-qualification-test; config_test service-admission-option-test.
Docs: stable-discovery-engine.md and v8-backend-modules-and-upgrade.md.
Battery 633 tests / 26,087 assertions / 0 failures; CLJS 193 / 7,311 / 0;
formal gate 506 obligations.
Two writers that both planned a :create of the same relationship against the same pre-write value both committed on DataScript and Datahike (the second add was a redundant datom) and both callers saw success, where the Datomic client and SpiceDB report :eacl/relationship-conflict to the loser (audit report 2026-08-15, section 2.19). tx-update-relationship now keeps the plan-time conflict for an already-present relationship and otherwise emits a transaction function, create-relationship-at-commit, that re-checks both endpoint values against the transaction-time database and returns the relationship adds or throws the typed conflict. DataScript (CLJ and CLJS) always runs it; Datahike runs it only under its default in-process writer (eacl.datahike.db/direct-writer?, now shared with the backend adapter) because a remote writer cannot transport a function value. Datahike reports a failing transaction function wrapped, so the client's transaction wrapper recovers the typed error from the cause chain (eacl.datahike.core/typed-transaction-error). Deterministic interleaving tests plan two creates against one pre-write value and commit both, on DataScript and on Datahike in both attribute representations. OpenSpec change serialize-create-conflicts added and archived into converged-relationship-storage; README, module READMEs and the audit report updated; AGENTS.md notes that cljs.main/-main calls shutdown-agents, so the CLJS build runs last on a shared nREPL.
Wire the physical execution layer (classified/retried reads, service-edge bulkhead, topology qualification) onto the routed engine
…p' into agent/serialize-create-conflicts # Conflicts: # formal/verification/public-source-closure.json
Serialize DataScript/Datahike :create conflicts at commit time
Stable-engine audit: report, dead-code sweep, gate repair, doc corrections, OpenSpec archive fold
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.
Summary
Replaces the v8 global entity-ID merge and the rejected symmetric fixed-point candidate with the accepted stable-discovery engine on every public entry point:
eacl.engine.sealed-plan): dense canonical ordinals, certified 0/1 storage-read-distance rank (untrusted generator, linear trusted checker), alternatives in(rank, ordinal)order, one composite fingerprint covering the complete order ABI.eacl.engine.stable-reducer): exact per-kind admission (merge points keyed by node + entity), logical release fixed at one value per transition (chunk-width order invariance), specialized admission keys, request-owned transients, typed checked limits, and an injectable read-demand seam for the future concurrency change.eacl.engine.stable-page)::stable-edgecursors through the existing authenticated relay envelope, latest-only history-free checkpoints carrying the undelivered lookahead segment, governed deterministic replay with boundary validation, typed stale/consistency-conflict/resource-exhaustion rejection.eacl.engine.physical): three-outcome read classification with cause codes and atomic partial discard, exact-descriptor retry under the original absolute deadline, service-edge admission with a replay ledger, closed topology capability record. The Datomic and Datahikeselect-exactpaths now classify failures instead of swallowingThrowableto nil.eacl.engine.stable-route) preserving the public error and truncation contracts.The dense first page costs 17 adapter commands versus the legacy merge's 60 on the same fixture (1 versus 2,002 on the adversarial 2,000-branch shape), removing the measured 148 s cold-page pathology at its cause.
Verification
formal/stable-discovery/verify-fast.sh, ~7 s).openspec/changes/adopt-stable-discovery-enumeration/,exploration/, anddocs/stable-discovery-engine.md.Notes
:stable-edge(one-based ordinals) and prior development cursors are rejected explicitly. EACL v8 is unreleased, so no migration is owed.