Enable v9 Caveats and expiring Relationships

.github/workflows/test.yml

@@ -141,7 +141,7 @@ jobs:
             "(do
                (require '[eacl.build.release :as release] :reload)
                (release/build-install-smoke
-                {:version \"8.0.0-SNAPSHOT\"}))"
+                {:version \"9.0.0-SNAPSHOT\"}))"
 
       - name: Run DataScript ClojureScript tests
         run: |

README.md

@@ -135,8 +135,7 @@ This README is too long & too technical, so I am working to simplify it and brea
 
 > [!WARNING]
 > EACL is used in production, but under active development.
-> EACL is [available on Clojars](https://clojars.org/dev.eacl/). Use the `8.0.0-SNAPSHOT`.
-> An official v8.0.0 release should be available by end-August 2026.
+> This branch targets `9.0.0-SNAPSHOT`. Build it locally until the coordinated release is published; see [Clojars](https://clojars.org/dev.eacl/) for published versions.
 
 ## Real-Time UI Maintenance
 
@@ -653,19 +652,19 @@ EACL supports multiple backends. Each adapter will bring in the shared EACL engi
 
 ```clojure
 ;; Datomic Pro
-{:deps {dev.eacl/eacl-datomic {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datomic {:mvn/version "9.0.0-SNAPSHOT"}}}
 
 ;; Datahike
-{:deps {dev.eacl/eacl-datahike {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datahike {:mvn/version "9.0.0-SNAPSHOT"}}}
 
 ;; DataScript
-{:deps {dev.eacl/eacl-datascript {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datascript {:mvn/version "9.0.0-SNAPSHOT"}}}
 
 ;; Datalevin (coordinate reserved; publication remains gated)
-{:deps {dev.eacl/eacl-datalevin {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datalevin {:mvn/version "9.0.0-SNAPSHOT"}}}
 
 ;; Core-only consumers and backend authors (you typically won't need this)
-{:deps {dev.eacl/eacl {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl {:mvn/version "9.0.0-SNAPSHOT"}}}
 ```
 
 ### Development from source
@@ -987,7 +986,7 @@ order.
 Add the Datomic adapter dependency to your `deps.edn` file:
 
 ```clojure
-{:deps {dev.eacl/eacl-datomic {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datomic {:mvn/version "9.0.0-SNAPSHOT"}}}
 ```
 
 ```clojure
@@ -1086,7 +1085,7 @@ Add the Datomic adapter dependency to your `deps.edn` file:
 For Clojure/JVM applications backed by Datahike, add the Datahike adapter dependency to your `deps.edn` file:
 
 ```clojure
-{:deps {dev.eacl/eacl-datahike {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datahike {:mvn/version "9.0.0-SNAPSHOT"}}}
 ```
 
 ```clojure
@@ -1140,7 +1139,7 @@ commit records.
 For server-side or browser demos, use the DataScript adapter:
 
 ```clojure
-{:deps {dev.eacl/eacl-datascript {:mvn/version "8.0.0-SNAPSHOT"}}}
+{:deps {dev.eacl/eacl-datascript {:mvn/version "9.0.0-SNAPSHOT"}}}
 ```
 
 ```clojure
@@ -1917,22 +1916,25 @@ but it is not a byte-for-byte or operational clone:
   sets unless your application explicitly sorts them; never compare EACL and
   SpiceDB page membership or cursor bytes.
 - EACL cursors bind the selected native revision and its dependency/order
-  proof. A cursor walk stays on that exact snapshot. If the backend cannot
-  reconstruct it, EACL fails closed. A relevant write does not silently change
-  page membership midway through a cursor walk.
+  proof. A cursor walk stays on that database snapshot. Qualified client-targeted
+  cursors capture fresh time and require restart when their temporal certificate
+  ends; explicit snapshots pin historical time. Neither mode silently rebases
+  its page boundary. Unavailable native history fails closed.
 - Omitted consistency means `:minimize-latency`. EACL selects the current
   immutable database value visible to the local backend connection. SpiceDB may use
   an optimized cached revision, so freshness can differ. Use each backend's
   own causal token with `at-least-as-fresh` or `at-exact-snapshot` when the
   distinction matters; tokens and cursors are backend-local.
 - EACL provides `count-resources`, `count-subjects`, a controllable EACL result
   cache, and `delete-object!`, which removes both stored Relationship halves.
-  Datomic commits high-degree deletion in batches of 1,000; Datahike and
-  DataScript use one atomic transaction. These do not have direct SpiceDB API
-  equivalents.
-- EACL currently supports a smaller schema subset: unions, intersections,
-  exclusions, and its documented arrow forms, but not caveats, wildcard
-  subjects, expiration, or subject relations.
+  Qualified deletion uses bounded native transactions; each transaction removes
+  both endpoint values and their owned qualifier together. These operations do
+  not have direct SpiceDB API equivalents.
+- V9 supports [Caveats and expiring Relationships](docs/caveats.md), including
+  conditional results and an exclusive UTC-millisecond expiry. Its bounded CEL
+  profile is a subset of SpiceDB's expression language; wildcard subjects and
+  subject relations remain unsupported. Qualified activation requires upgrading
+  every serving Peer first.
 - EACL evaluates relationship cycles as a fixed point and has no separate
   dispatch-depth limit for checks, lookups, and counts. These operations remain
   subject to configured traversal work limits. SpiceDB uses a configurable
@@ -1960,4 +1962,4 @@ Some of this open-source work was generously funded by my former employer, [Clou
 
 - EACL is free and open-source, licensed under the Eclipse Public License v2.0.
 
-See [Caveat and qualifier foundation](docs/caveats.md) for the staged profile, optional JVM evaluator, and Phase 3 serving boundary.
+See [Caveats and expiring Relationships](docs/caveats.md) for the v9 public APIs, optional JVM evaluator, trusted-clock and cursor semantics, and coordinated rollout.

bin/formal

@@ -162,7 +162,8 @@ command=${1:-}
 case "$command" in
   fast)
     need_tools
-    exec sh "$repo_root/formal/caveats/verify-fast.sh"
+    sh "$repo_root/formal/caveats/verify-fast.sh"
+    exec sh "$repo_root/formal/qualified/verify-fast.sh"
     ;;
   bootstrap)
     exec "$repo_root/bin/bootstrap-formal-tools"

docs/benchmarks/qualified-authorization-budgets.edn

@@ -0,0 +1,20 @@
+{:version 1
+ :recorded-before-measurement true
+ :documents 1000
+ :backends [:datascript :datomic :datahike :datalevin]
+ :cases [:ordinary :sparse-5 :sparse-10 :qualified-prefix-10 :expired-prefix-10]
+ :samples 100
+ :relative-budgets
+ {:ordinary {:latency-factor 1.5 :latency-slack-ns 100000
+             :allocation-factor 1.5 :allocation-slack-bytes 32768}
+  :sparse-5 {:latency-factor 2.0 :latency-slack-ns 250000
+             :allocation-factor 2.0 :allocation-slack-bytes 65536}
+  :sparse-10 {:latency-factor 3.0 :latency-slack-ns 500000
+              :allocation-factor 3.0 :allocation-slack-bytes 131072}
+  :qualified-prefix-10 {:latency-factor 5.0 :latency-slack-ns 2000000
+                        :allocation-factor 5.0 :allocation-slack-bytes 524288}
+  :expired-prefix-10 {:latency-factor 5.0 :latency-slack-ns 2000000
+                      :allocation-factor 5.0 :allocation-slack-bytes 524288}}
+ :absolute-p95-ns {:point 5000000 :cache-hit 250000 :page 250000000 :count 2000000000}
+ :data-read-budgets {:ordinary 0 :cache-hit 0 :maximum-per-qualifier 1
+                     :maximum-per-shared-definition 1 :maximum-per-relation 1}}

docs/benchmarks/qualified-authorization.md

@@ -0,0 +1,77 @@
+# Qualified authorization release qualification
+
+The numerical budgets in `qualified-authorization-budgets.edn` were recorded
+before running the semantic workload. They are local release regression limits,
+not service latency promises. A failed limit blocks acceptance; changing a limit
+requires a documented reason and a fresh comparison, not silently accepting a
+slower result.
+
+Compare the disabled epoch's ordinary graph with the enabled epoch on the same
+host, backend, graph size, public operation, and cache mode. The ordinary case
+allows 1.5 times baseline plus 100 microseconds and 32 KiB per request for request
+scope/certificate construction. Sparse 5% and 10% cases allow respectively
+2 and 3 times baseline plus 250/500 microseconds and 64/128 KiB. Concentrated
+10% cases allow 5 times baseline plus 2 milliseconds and 512 KiB because a
+bounded output page may have to examine an inactive prefix. Both median and
+p95 batch latency must meet the relative limit. Absolute p95 limits are 5 ms
+for points, 250 microseconds for completed-answer hits, 250 ms for a 50-item
+page, and 2 seconds for an exact 1,000-document count. These limits deliberately
+include public request selection, admission, context, and result construction.
+
+The workload uses the actual optional JVM CEL evaluator. It measures direct,
+negative, exclusion, arrow, recursive, first-page, continuation, exact-count,
+and completed-answer-hit operations. Qualifiers are distributed over the
+entire generated Relationship set; the report records exact counts and density.
+Qualified prefixes use active Caveats/expiry, while expired prefixes exercise
+skipping before Caveat evaluation, including subtracting Relationships. Each
+document also has a parent edge, and every fourth document has a ban.
+
+Cold requests disable answer and decoded-data caches. Warm requests use the
+same fixed context and `:populate-cache? false`, after public physical
+Relationship inspection populates decoded data without publishing authorization
+answers. Both epochs therefore perform fresh authorization; the harness rejects
+unexpected completed-answer hits. The compiled-program cache remains independent.
+Completed-answer-hit requests instead keep publication enabled and their context
+fixed. The clock is fixed within each case; advancing-clock correctness is
+covered by the native cache trace and cursor conformance gates.
+
+An initial warm prototype varied an unused context field. That was an invalid
+isolation method: the ordinary epoch could reuse internal decisions while the
+qualified epoch correctly included the whole context in its scope. Measurement
+version 3 replaces that prototype with public read-only cache requests and data
+preloading on both epochs. No latency or allocation threshold was changed.
+
+JVM allocation is measured with the current thread's allocation counter and
+excludes asynchronous backend work. The backend matrix, raw batch samples,
+runtime/host information, first-call latency, and measured native qualification
+reads must be retained with the result. Read instrumentation is separate from
+timing: ordinary edges and completed-answer hits must perform zero qualifier
+data reads; a cold request may fetch each qualifier, shared definition, and
+Relation at most once. Each operation warms for at least one second before 100 measured batches.
+Counts use five requests per batch, pages three, and points 10–50, as recorded
+in each metric. These are percentiles of batch means, not a per-request tail
+latency claim. The longer warmup, larger sample count, and count/page batches were introduced
+after single-request samples exposed compilation/pause sensitivity near the
+fixed limits; the latency and allocation thresholds were not changed. Continuation timing includes
+both the first page and its resume under the same context. Completed-answer
+hits use the root grant, which is qualified in every nonzero-density case, and
+must report an actual answer-cache hit with zero qualification-data reads.
+
+Run the benchmark through the project nREPL with `:datalevin-dev:caveats-jvm`
+loaded. The harness is in `eacl.bench.qualified-authorization-test`; regular unit
+test runs do not execute benchmarks. Release acceptance requires all four
+backend reports and the checked budget comparison. ClojureScript semantic
+correctness is separately gated by the advanced Node suite; these JVM allocation
+and latency limits do not claim to measure JavaScript or networked deployments.
+
+Measurement version 4 adds an assertion that the first 20 physical member
+Relationships actually form the intended native qualified/expired prefix. Runs
+use a fresh JVM per backend with `-Xms512m -Xmx2g` and no concurrent test or proof
+work, so retained state from earlier test suites does not affect measurements.
+Version 5 retains that protocol after optimizing definition-content reuse. The
+checker rejects duplicate reports, mixed versions/budgets, missing operations,
+and incomplete sample sets.
+
+The [2026-09-05 accepted matrix](results/qualified-authorization-2026-09-05/README.md)
+contains all 24 reports, raw samples, source provenance, and the 1,440 passing
+budget comparisons.

docs/benchmarks/results/qualified-authorization-2026-09-05/README.md

@@ -0,0 +1,20 @@
+# Qualified authorization performance acceptance
+
+All 24 reports passed all 1,440 fixed latency and allocation comparisons. Each report contains 18 operation/cache-mode combinations and 100 measured batches per combination. Ordinary edges and completed-answer hits issued zero qualification-data reads; no request fetched a qualifier, shared definition, or Relation more than once.
+
+This run measures implementation commit `89e25860f198c1c00279e78e047d962ae902077b`, explicitly binding each semantic epoch before the default-v9 activation. The activation changes the default and release/continuation ABI metadata; the benchmark already selects each evaluated epoch explicitly.
+
+The workload has 1,000 documents and 2,253 Relationships. The sparse cases have 112 (4.97%) and 225 (9.99%) qualified Relationships. Measurements used macOS 26.4.1, Apple M4 Max, 36 GiB RAM, and Java 26.0.2, with a fresh 2 GiB maximum-heap JVM per backend and no concurrent tests, proof runs, or builds.
+
+Exact-count median latency, milliseconds (cold cache):
+
+| Backend | Legacy 0% | V9 0% | V9 5% | V9 10% | Qualified prefix | Expired prefix |
+|---|---:|---:|---:|---:|---:|---:|
+| datascript | 1.519 | 1.764 | 2.560 | 3.670 | 3.229 | 2.455 |
+| datomic | 1.659 | 1.842 | 2.863 | 4.131 | 4.608 | 3.536 |
+| datahike | 1.736 | 1.898 | 2.976 | 4.067 | 3.609 | 2.793 |
+| datalevin | 23.033 | 23.664 | 24.970 | 26.310 | 25.868 | 28.634 |
+
+The [CSV](metrics.csv) contains first-call latency, medians, p95 batch means, allocations, sample counts, and native read counts for every operation. These percentiles describe batch means, not individual-request tail latency or a service-level promise. The [raw archive](raw-reports.tar.gz) retains every batch sample and budget; [provenance](provenance.json) pins production source hashes, the benchmark, dependency declarations, and the Datalevin fork commit. The executable checker result is [budget-comparison.edn](budget-comparison.edn).
+
+Earlier prototype/isolation runs failed fixed limits and led to changes in compiled-definition reuse and measurement isolation. Those failures were not accepted as release evidence. Version 5 uses the documented fresh-JVM, fixed-context protocol and the original numeric budgets without relaxation. The complete protocol and limits are in [the benchmark guide](../../qualified-authorization.md).

docs/benchmarks/results/qualified-authorization-2026-09-05/budget-comparison.edn

@@ -0,0 +1 @@
+{:reports 24, :comparisons 1440, :passed? true, :failures []}