Deploy v8 SNAPSHOT to Clojars - #122
Merged
Merged
Conversation
…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
Add cooperative cancellation to EACL reads
Adopt stable-discovery enumeration: sealed plans, width-one reducer, stable cursors
[v8.0] Add cache, recursive schema, backend modules, and verified engine
Permission-tree expansion accepts a relation as its root and then reads that relation's relationships, but no permission path names the relation, so its dependency closure was empty. An empty closure resolves to a complete proof with dependency stamp 0, which the managed cross-snapshot tier treats as equal at every later snapshot: once expansion became cacheable, a relation-rooted tree survived the relationship writes it reports. The closure now includes the relation definitions of any node with no permission paths, on both the Datomic and shared orchestration paths. Also from the same review: - Weigh nested answers by retained collection entries. Permission trees carry their payload in :intermediate/:leaf nodes rather than a :data vector, so every tree was admitted at the 512-byte floor and the weight budget stopped bounding what the answer tiers retain. `some?` guards the page branch because ClojureScript and Clojure disagree on `(counted? nil)`. - Require adapter determinism to MINT a snapshot-exact identity, not merely to read one. A client whose adapter readers refuse was still seeding the tier with entries none of its exact requests could consult. - Stop republishing to the snapshot-exact tier on every exact-current hit. The answer is offered when computed or promoted; republishing re-ran the answer validator and weight function on the hot path and recorded a publication race against the entry it had just found. - Bypass the snapshot-exact tier when an adapter cannot mint a canonical identity, instead of failing the request. A cache that cannot key an answer is a caching limit, and nil is the documented outcome for such views. - Report the selected snapshot as an exact hit's cache basis rather than copying the entry's, which may have been retained from an answer computed at an earlier basis. - Cancel the Datomic sync future when a causal-floor or authoritative-head wait stops waiting, as targeted exact catch-up already does. Both keep their established failure taxonomy. - Refuse exact-snapshot consistency for d/filter, d/since and d/history views, which report their origin's database id and basis and would otherwise mint the same snapshot identity as the plain value while answering a different question. - Await an unobserved revision in Datahike exact selection under the caller's bound, so a lagging reader reports bounded lag rather than missing history. - Bound cursor reconstruction by the request's remaining execution time, as every other selection path already is. - Consume the selected context's :snapshot-exact? instead of recomputing it, and drop the :completed-cache? field that had become a constant. - Refresh the change's delta specs against the main specs they edited, so the change can archive.
Datahike has no `d/sync` (replikativ/datahike#958), so the only ways to wait for a revision the local value has not observed are unbounded polling or a fixed N-second timeout, and neither distinguishes a revision that is merely late from one that will never arrive. Listeners are not an option either: they fire only for transactions made through the connection that registered them. Exact selection therefore reports a revision above the local head as unavailable immediately, restoring the guard this branch had replaced with a bounded await, and leaves the deadline for the caller to spend. Retained history at or below the local head still resolves without waiting, and `:select-at-least` keeps its await, which is the operation whose contract is to wait. The local head is also more authoritative than it first appears: Datahike caches connections per store config in-process, so two `connect` calls with one config return the same object and a direct writer cannot lag itself. The regression test now asserts the unavailable result and that selection returns without spending the caller's timeout.
Fix cache correctness and bounds found reviewing exact-snapshot reuse
Cursors no longer expire, `at-exact-snapshot` now calls `(d/sync T)` if Peer is behind and exact queries now leverage Exact Answer cache
Improve the EACL v8 README
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.
No description provided.