diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index b74dbc300..43fb8e488 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -608,12 +608,10 @@ jobs: sh bin/ci-nrepl-eval 7788 \ "(do (require 'eacl.formal.generators-test :reload) - (require 'eacl.formal.cache-strategy-adversarial-test :reload) (require 'eacl.formal.mutation-control-test :reload) (let [result (clojure.test/run-tests 'eacl.formal.generators-test - 'eacl.formal.cache-strategy-adversarial-test 'eacl.formal.mutation-control-test)] (when (pos? (+ (:fail result 0) (:error result 0))) (throw (ex-info \"generator/mutation controls failed\" result))) diff --git a/docs/benchmarks/operator-engine.md b/docs/benchmarks/operator-engine.md index a1c2fc253..51075bbce 100644 --- a/docs/benchmarks/operator-engine.md +++ b/docs/benchmarks/operator-engine.md @@ -14,7 +14,7 @@ Use a project nREPL with the `:dev:test` aliases: ```sh clj-nrepl-eval -p "(require 'eacl.engine.physical-route-test :reload) (clojure.test/run-tests 'eacl.engine.physical-route-test)" -clj-nrepl-eval -p "(require 'eacl.operator-engine.experiments-test :reload) (clojure.test/run-tests 'eacl.operator-engine.experiments-test)" +clj-nrepl-eval -p "(require 'eacl.operator-engine.experiments :reload) (eacl.operator-engine.experiments/run-all)" clj-nrepl-eval -p "(require 'eacl.baseline.perf :reload) (eacl.baseline.perf/capture-perf!)" ``` diff --git a/docs/release-notes-v8.0.md b/docs/release-notes-v8.0.md index 18d1ae813..61bafd70d 100644 --- a/docs/release-notes-v8.0.md +++ b/docs/release-notes-v8.0.md @@ -289,12 +289,13 @@ Caller-supplied cache providers are rejected at construction because they do not control the native completed-answer or continuation stores. Continuation state remains isolated in a bounded private store. -`:cache-attempt` now names only controls the live private-cache path consumes: -`:evaluation-reserve-ms` (default `10`) and -`:maximum-atomic-attempts` (default `4`). Decorative stage-timeout, -encoded-byte, decoded-weight, and candidate-count controls are rejected. Native -per-tier/per-entry weights remain construction-time cache limits, while the -single request `:timeout-ms` remains the end-to-end deadline. +`:cache-attempt` is not an option. `make-client` rejects it as an unknown key +with `:eacl/invalid-config`, and a request that carries it is rejected as an +unknown key as well. There are no evaluation-reserve, publication-attempt, +stage-timeout, byte, weight, or candidate-count controls. Cache capacity is a +positive entry count per store, set under `:cache` at construction (see +[cache behavior and recovery](cache.md)), and the single request `:timeout-ms` +remains the end-to-end deadline. Bounded reads also accept a per-request `:cancellation-token` created by `eacl.core/cancellation-token`. `eacl.core/cancel!` is idempotent; the next diff --git a/formal/baselines/recursive-op-count-envelopes.edn b/formal/baselines/recursive-op-count-envelopes.edn index 5c94bec4c..3fc738a4f 100644 --- a/formal/baselines/recursive-op-count-envelopes.edn +++ b/formal/baselines/recursive-op-count-envelopes.edn @@ -21,7 +21,6 @@ {:maximum-proof-frame-reads 3 :maximum-plan-compiles 1 ; 3.3 ratchet: nil-store lookup deleted the duplicate :maximum-denotation-key-builds 0 ; 3.3 ratchet: no key work without a store - :maximum-denotation-dependency-calcs 0 ; 3.3 ratchet :maximum-permission-path-calcs 11 ; engine-direct raw (no request ; context bound); the Datomic facade ; path measures 1 via 3.2's memo. @@ -37,7 +36,6 @@ {:maximum-proof-frame-reads 0 :maximum-plan-compiles 1 :maximum-denotation-key-builds 0 - :maximum-denotation-dependency-calcs 0 :maximum-backend-scans 8} ; bounded reverse point check :client-lookup-first-50 {:maximum-proof-frame-reads 5 diff --git a/formal/counterexamples/EACL-FORMAL-002/entry.edn b/formal/counterexamples/EACL-FORMAL-002/entry.edn index b92a76310..d9721a916 100644 --- a/formal/counterexamples/EACL-FORMAL-002/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-002/entry.edn @@ -12,6 +12,7 @@ "Datomic clients may retain an explicitly requested complete denotation in bounded client-private storage keyed by the selected immutable snapshot and complete semantic root. Later pages slice that denotation without backend traversal; unavailable artifacts replay from one independently selected immutable snapshot." :closing-evidence ["eacl.datomic.lookup-cache-test/recursive-cursors-resume-from-the-client-private-denotation-test" - "eacl.datomic.lookup-cache-test/recursive-cursors-replay-across-independent-client-proofs-test" - "eacl.bench.pagination-test/recursive-traversal-prefix-benchmark" - "eacl.bench.pagination-test/recursive-page-size-work-benchmark"]} + ;; Historical: eacl.bench.pagination-test/recursive-traversal-prefix-benchmark + ;; and recursive-page-size-work-benchmark were retired with the analysis + ;; router (3395d961). + "eacl.datomic.lookup-cache-test/recursive-cursors-replay-across-independent-client-proofs-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-003/entry.edn b/formal/counterexamples/EACL-FORMAL-003/entry.edn index dd4407ad7..412aba753 100644 --- a/formal/counterexamples/EACL-FORMAL-003/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-003/entry.edn @@ -11,5 +11,8 @@ :fix "authenticated-store first passed the semantic kind through to the weighted provider (with :authenticated-v3 only as a compatibility fallback); trusted-surface-hygiene 11.1 then deleted the adapter outright — its only consumer was the write-only :shared-cache-store option nothing read — so the defective surface no longer exists to regress." :closing-evidence - ["eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test" - "eacl.bench.pagination-test/permission-check-benchmark"]} + [;; Historical: eacl.bench.pagination-test/permission-check-benchmark was + ;; retired with the analysis router (3395d961). + ;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.datomic.lookup-cache-test/cache-config-is-validated-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-004/entry.edn b/formal/counterexamples/EACL-FORMAL-004/entry.edn index 36e4c21cc..ea55e9bff 100644 --- a/formal/counterexamples/EACL-FORMAL-004/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-004/entry.edn @@ -12,6 +12,9 @@ "Every cursor is authenticated to the complete semantic query. Non-exact continuation re-evaluates on one selected current graph, without treating proof equivalence as authorization; explicit at-exact-snapshot continuation alone selects retained history." :closing-evidence ["eacl.datomic.cache-review-regressions-test/proofless-cursor-falls-back-to-exact-snapshot-test" - "eacl.relay-test/non-exact-continuation-recovers-on-current-graph-test (CLJ and CLJS)" - "formal/dafny/TemporalSafety.dfy recovery-mode lemmas" + ;; Historical: eacl.relay-test/non-exact-continuation-recovers-on-current-graph-test + ;; and the recovery-mode lemmas were removed with cursor recovery + ;; (7a3cd3e6). The two lemmas below are what TemporalSafety.dfy has now. + "formal/dafny/TemporalSafety.dfy/MissingProofCannotLiftAcrossGraphs" + "formal/dafny/TemporalSafety.dfy/ExactContinuationUsesRetainedAuthenticatedGraph" "formal/tla/EaclTemporal.tla CursorCurrentSafe invariant"]} diff --git a/formal/counterexamples/EACL-FORMAL-008/entry.edn b/formal/counterexamples/EACL-FORMAL-008/entry.edn index b47a4c738..263d831b4 100644 --- a/formal/counterexamples/EACL-FORMAL-008/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-008/entry.edn @@ -11,5 +11,7 @@ :fix "The final v8 cache removes the external proof-provider resolution surface. Current-generation and managed native cache paths own their bounded proof reads; the deleted eacl.cache/resolve! provider callback path cannot abort authorization." :closing-evidence - ["eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test" - "eacl.formal.executed-mutation-controls/cache-fail-open-killed?"]} + [;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.datomic.lookup-cache-test/cache-config-is-validated-test" + "formal/mutations/registry.edn :cache-fail-open"]} diff --git a/formal/counterexamples/EACL-FORMAL-010/entry.edn b/formal/counterexamples/EACL-FORMAL-010/entry.edn index fa07bbd59..78b99d8d2 100644 --- a/formal/counterexamples/EACL-FORMAL-010/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-010/entry.edn @@ -12,9 +12,9 @@ "Generated worklist authority is restricted to roots that transitively depend on a recursive SCC, whose public contract is traversal order. Direct and acyclic roots retain the optimized ordered merge. Dafny proves ordered step and bounded-chunk reconstruction; generated Java and JavaScript are differential oracles. Per-EID generated routing failed the performance gate, so source-digested specialization refinement and independent review remain release gates." :closing-evidence ["eacl.formal.state-trace-differential-test/generated-decisions-and-source-specialized-acyclic-paths-preserve-order-and-point-locality" - "eacl.formal.production-kernel-test/optimized-jvm-ordered-merge-refines-generated-chunks" - "eacl.formal.production-kernel-test/optimized-javascript-ordered-merge-refines-generated-chunks" + ;; Historical: eacl.formal.production-kernel-test/optimized-jvm-ordered-merge-refines-generated-chunks + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). + ;; formal/verification/performance-gates.edn and indexed-traversal.edn + ;; were generated evidence ledgers, removed in 483911d6. "formal/dafny/OrderedMerge.dfy AscendingChunkReconstructsMerge and DescendingChunkReconstructsMerge" - "formal/mutations/registry.edn :ordered-merge-wrong-comparator" - "formal/verification/performance-gates.edn :rejected-acyclic-generated-prototype" - "formal/verification/indexed-traversal.edn explicitly withholds acyclic generated authority"]} + "formal/mutations/registry.edn :ordered-merge-wrong-comparator"]} diff --git a/formal/counterexamples/EACL-FORMAL-011/entry.edn b/formal/counterexamples/EACL-FORMAL-011/entry.edn index 09c933e7b..e4f92079b 100644 --- a/formal/counterexamples/EACL-FORMAL-011/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-011/entry.edn @@ -11,6 +11,6 @@ :fix "The host reverse evaluator now queues consumer registration before the dependent goal, matching the generated transition system. Shadow mode independently captures cache-free host and generated counters plus retained logical units and compares them without disclosing authorization values." :closing-evidence - ["eacl.formal.state-trace-differential-test/recursive-shadow-compares-complete-public-results" + ["eacl.formal.state-trace-differential-test/recursive-generated-authority-covers-complete-public-results" "eacl.backend.v8-test reverse traversal characterization" "DataScript CLJS full suite: 127 tests, 4165 assertions"]} diff --git a/formal/counterexamples/EACL-FORMAL-013/entry.edn b/formal/counterexamples/EACL-FORMAL-013/entry.edn index 9a5b34ea0..5071803df 100644 --- a/formal/counterexamples/EACL-FORMAL-013/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-013/entry.edn @@ -11,5 +11,9 @@ :fix "The final v8 cache has no registered flights. Read-only lookup never starts work; identical misses compute independently and can only race bounded nonblocking publication, so self-wait is structurally impossible." :closing-evidence - ["eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test" - "eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test"]} + [;; Historical: eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + ;; exercised a model defined in its own file. + ;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test" + "eacl.subproblem-cache-test/publication-validation-runs-once-and-never-on-hit-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-014/entry.edn b/formal/counterexamples/EACL-FORMAL-014/entry.edn index f6206776b..5efb98093 100644 --- a/formal/counterexamples/EACL-FORMAL-014/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-014/entry.edn @@ -13,5 +13,8 @@ :fix "The final v8 cache deletes computation slots, permits, shared flights, and recursive self-bypass. Every miss performs its own request-bounded computation and publication is a bounded nonblocking optimization." :closing-evidence - ["eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test" - "eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test"]} + [;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + ;; Historical: eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + ;; exercised a model defined in its own file. + "eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-015/entry.edn b/formal/counterexamples/EACL-FORMAL-015/entry.edn index 159dc61cd..ae50d88d5 100644 --- a/formal/counterexamples/EACL-FORMAL-015/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-015/entry.edn @@ -13,5 +13,6 @@ :fix "The final v8 cache deletes flight selection and store locks. Independent work captures one opaque lifecycle; clear replaces it, and bounded compare-and-set publication rejects a detached lifecycle without waiting or mutating the new generation." :closing-evidence - ["eacl.cache-test/lifecycle-rotation-detaches-data-and-content-revision-test" - "eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test"]} + [;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.datascript.snapshot-lifecycle-test/full-rotation-detaches-every-runtime-cache-child-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-016/entry.edn b/formal/counterexamples/EACL-FORMAL-016/entry.edn index 873f3435b..9e48ae2c1 100644 --- a/formal/counterexamples/EACL-FORMAL-016/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-016/entry.edn @@ -13,5 +13,6 @@ :fix "The final v8 cache makes lookup read-only and removes flight installation. A miss never mutates state or starts work; independent computation precedes a separate bounded compare-and-set publication transition." :closing-evidence - ["eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test" + [;; Historical: eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + ;; exercised a model defined in its own file. "eacl.subproblem-cache-test/publication-validation-runs-once-and-never-on-hit-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-017/entry.edn b/formal/counterexamples/EACL-FORMAL-017/entry.edn index e2243c09d..aedbc2691 100644 --- a/formal/counterexamples/EACL-FORMAL-017/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-017/entry.edn @@ -13,5 +13,8 @@ :fix "The final v8 cache removes coordinator flights and join behavior. Unrepresented misses compute independently and may only race bounded publication of completed values; no request changes its answer to or waits for another in-flight request." :closing-evidence - ["eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test" - "eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test"]} + [;; Historical: eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + ;; exercised a model defined in its own file. + ;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-018/entry.edn b/formal/counterexamples/EACL-FORMAL-018/entry.edn index 5dd6aaa1a..b98378f7d 100644 --- a/formal/counterexamples/EACL-FORMAL-018/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-018/entry.edn @@ -13,5 +13,6 @@ :fix "The final v8 cache removes registered flights and the selection lock. Completion only attempts bounded compare-and-set publication against its captured lifecycle; a cleared lifecycle rejects the detached publication without blocking." :closing-evidence - ["eacl.cache-test/lifecycle-rotation-detaches-data-and-content-revision-test" - "eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test"]} + [;; Historical: eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + ;; asserted only that the deleted names stayed absent. + "eacl.datascript.snapshot-lifecycle-test/full-rotation-detaches-every-runtime-cache-child-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-022/entry.edn b/formal/counterexamples/EACL-FORMAL-022/entry.edn index 83420f7a1..6979cc2aa 100644 --- a/formal/counterexamples/EACL-FORMAL-022/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-022/entry.edn @@ -13,5 +13,5 @@ :fix "Generated traversal errors now recover the exact configured limit from the validated limit map without adding generated-only direction data, and the redacted shadow projection compares bounded numeric limit fields internally while diagnostics continue to expose only changed field names and result variants." :closing-evidence - ["eacl.formal.state-trace-differential-test/recursive-shadow-compares-complete-public-results" + ["eacl.formal.state-trace-differential-test/recursive-generated-authority-covers-complete-public-results" "formal mutation :shadow-typed-error-omits-limit"]} diff --git a/formal/counterexamples/EACL-FORMAL-023/entry.edn b/formal/counterexamples/EACL-FORMAL-023/entry.edn index 946b1e804..8fa7a1269 100644 --- a/formal/counterexamples/EACL-FORMAL-023/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-023/entry.edn @@ -13,6 +13,6 @@ :fix "Generated render rejection now preserves the established legacy stale-cursor public shape, and a raw-engine shadow trace deletes the cursor result before continuation so the generated and legacy failures are compared." :closing-evidence - ["eacl.formal.state-trace-differential-test/recursive-shadow-compares-stale-cursor-error-shape" - "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-compare-generated-javascript" + ["eacl.formal.state-trace-differential-test/generated-stale-cursor-error-shape" + "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-use-generated-javascript" "formal mutation :shadow-generated-stale-cursor-adds-direction"]} diff --git a/formal/counterexamples/EACL-FORMAL-024/entry.edn b/formal/counterexamples/EACL-FORMAL-024/entry.edn index c83df6f50..fefeb3df4 100644 --- a/formal/counterexamples/EACL-FORMAL-024/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-024/entry.edn @@ -14,5 +14,5 @@ "The materialized model now treats queuedWork as the maximum observed pending-work cardinality, checks the current queue cardinality directly against maxQueuedWork, and retains cumulative enqueue accounting as a separate resource dimension outside this safety limit." :closing-evidence ["eacl.formal.production-kernel-test/generated-materialized-queue-limit-is-instantaneous" - "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-compare-generated-javascript" + "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-use-generated-javascript" "formal mutation :materialized-queue-limit-counts-cumulative-enqueues"]} diff --git a/formal/counterexamples/EACL-FORMAL-025/entry.edn b/formal/counterexamples/EACL-FORMAL-025/entry.edn index b389e1473..f9f50c5a9 100644 --- a/formal/counterexamples/EACL-FORMAL-025/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-025/entry.edn @@ -14,5 +14,5 @@ "Materialized completion remains a semantic value oracle only. Production limit and dimensional-counter refinement is now assigned exclusively to the generated indexed state machine under its certified ordered-adapter contract, and reports prohibit cross-scope resource substitution." :closing-evidence ["eacl.formal.production-kernel-test/materialized-resource-limits-are-whole-closure-scoped" - "eacl.formal.state-trace-differential-test/recursive-shadow-queue-limit-is-query-local" + "eacl.formal.state-trace-differential-test/generated-queue-limit-is-query-local" "formal mutation :materialized-resource-counter-promoted-to-production"]} diff --git a/formal/counterexamples/EACL-FORMAL-026/entry.edn b/formal/counterexamples/EACL-FORMAL-026/entry.edn index f055594b0..4bd423dcb 100644 --- a/formal/counterexamples/EACL-FORMAL-026/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-026/entry.edn @@ -13,6 +13,6 @@ :fix "Uncached recursive traversal and generated render rejection now expose one minimal stable public stale-cursor map containing only :eacl/error. Internal cursor and generated-render diagnostics are not part of public ExceptionInfo data, and regressions compare the entire map." :closing-evidence - ["eacl.formal.state-trace-differential-test/recursive-shadow-compares-stale-cursor-error-shape" - "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-compare-generated-javascript" + ["eacl.formal.state-trace-differential-test/generated-stale-cursor-error-shape" + "eacl.formal.production-kernel-test/datascript-public-recursive-cache-modes-use-generated-javascript" "formal mutation :generated-stale-cursor-leaks-render-details"]} diff --git a/formal/counterexamples/EACL-FORMAL-028/entry.edn b/formal/counterexamples/EACL-FORMAL-028/entry.edn index cb1cbca7c..60f8def12 100644 --- a/formal/counterexamples/EACL-FORMAL-028/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-028/entry.edn @@ -13,4 +13,6 @@ :fix "The obsolete multi-artifact manifest gate was retired. The executable production ClojureScript test rebuilds the runtime, enforces payload ceilings that affect browser performance, and rejects generated-oracle code in the production graph." :closing-evidence - ["eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test"]} + [;; Historical: eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test + ;; asserted only the text of the smoke tests. + "eacl.formal.cljs-production-gate-test/production-cljs-bundle-is-native-small-and-oracle-free-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-030/entry.edn b/formal/counterexamples/EACL-FORMAL-030/entry.edn index 1325cf86e..66a08577e 100644 --- a/formal/counterexamples/EACL-FORMAL-030/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-030/entry.edn @@ -15,6 +15,8 @@ :closing-evidence ["RecursiveEngine.RoutingTraversalScanIsExact" "RecursiveEngine.DecideTypedTraversalPermission" - "eacl.formal.production-kernel-test/generated-java-classifies-production-recursive-routing" - "eacl.formal.production-kernel-test/generated-javascript-classifies-production-recursive-routing" + ;; Historical: eacl.formal.production-kernel-test/generated-java-classifies-production-recursive-routing + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). + "eacl.formal.production-kernel-test/generated-java-checks-linear-routing-certificates" + "eacl.formal.production-kernel-test/generated-javascript-checks-linear-routing-certificates" "formal mutation :routing-node-identity-drops-resource-type"]} diff --git a/formal/counterexamples/EACL-FORMAL-031/entry.edn b/formal/counterexamples/EACL-FORMAL-031/entry.edn index 2e02ee9ee..56d44a8c9 100644 --- a/formal/counterexamples/EACL-FORMAL-031/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-031/entry.edn @@ -13,4 +13,6 @@ :fix "The obsolete Babashka manifest gate and exact tool-version assertion were removed. Production ClojureScript size and graph checks run as ordinary executable tests against freshly built bundles." :closing-evidence - ["eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test"]} + [;; Historical: eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test + ;; asserted only the text of the smoke tests. + "eacl.formal.cljs-production-gate-test/production-cljs-bundle-is-native-small-and-oracle-free-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-032/entry.edn b/formal/counterexamples/EACL-FORMAL-032/entry.edn index 72d4973ed..3c131b117 100644 --- a/formal/counterexamples/EACL-FORMAL-032/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-032/entry.edn @@ -13,6 +13,8 @@ :fix "The portable boundary now canonicalizes and compares the complete public ExceptionInfo data map internally. Diagnostics retain only changed top-level field names and typed error keywords. Untyped or non-portable exception data is reported as comparison-unavailable instead of silently passing." :closing-evidence - ["eacl.verified-kernel-test/shadow-error-comparison-covers-complete-portable-ex-data" - "eacl.verified-kernel-test/shadow-error-comparison-reports-unavailable-nonportable-data" + [;; Historical: eacl.verified-kernel-test/shadow-error-comparison-covers-complete-portable-ex-data + ;; and shadow-error-comparison-reports-unavailable-nonportable-data were + ;; removed with shadow mode (d96bc4c6). + "eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test" "formal mutation :shadow-typed-error-drops-portable-values"]} diff --git a/formal/counterexamples/EACL-FORMAL-033/entry.edn b/formal/counterexamples/EACL-FORMAL-033/entry.edn index 74b35179b..07dcc4fd9 100644 --- a/formal/counterexamples/EACL-FORMAL-033/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-033/entry.edn @@ -13,5 +13,7 @@ :fix "Complete-public shadow comparison identifies a selected graph by source scope, snapshot identity, graph anchor, and order hint. It excludes the client-local exact locator while retaining separate exact-locator reconstruction and resolved-graph postcondition tests." :closing-evidence - ["eacl.formal.state-trace-differential-test/public-shadow-compares-cache-provenance-and-selected-graph" - "formal mutation :graph-identity-includes-client-local-exact-locator"]} + [;; Historical: eacl.formal.state-trace-differential-test/public-shadow-compares-cache-provenance-and-selected-graph + ;; was removed with shadow mode (d96bc4c6), and the mutation + ;; :graph-identity-includes-client-local-exact-locator in 2ebf7437. + "eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-034/entry.edn b/formal/counterexamples/EACL-FORMAL-034/entry.edn index cefea75c7..cd10e1a46 100644 --- a/formal/counterexamples/EACL-FORMAL-034/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-034/entry.edn @@ -14,5 +14,6 @@ "The launcher now calls cljs.build.api/build, runs the Node suite, and asserts through the same nREPL that a future still completes. Formal evidence no longer depends on whether CLJS compilation ran before JVM concurrency tests." :closing-evidence ["formal/smoke/cljs/run runtime postcondition :eacl.formal/agent-executor-alive" - "eacl.characterization-fixture-test/formal-cljs-smoke-preserves-persistent-nrepl-executors-test" + ;; Historical: eacl.characterization-fixture-test/formal-cljs-smoke-preserves-persistent-nrepl-executors-test + ;; asserted only the text of the launcher and of formal.yml. "formal mutation :formal-cljs-smoke-terminates-agent-executors"]} diff --git a/formal/counterexamples/EACL-FORMAL-036/entry.edn b/formal/counterexamples/EACL-FORMAL-036/entry.edn index a495f1722..054878a30 100644 --- a/formal/counterexamples/EACL-FORMAL-036/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-036/entry.edn @@ -16,6 +16,8 @@ ["eacl.formal.production-kernel-test/generated-java-continues-pages-from-verified-lookahead" "eacl.engine.continuation-reuse-test/repeated-pagination-reuses-checkpoints-test" "eacl.engine.physical-route-test/anchored-point-check-test" - "eacl.datascript.contract-test/cold-recursive-point-check-publishes-complete-fixed-point-test" + ;; Historical: eacl.datascript.contract-test/cold-recursive-point-check-publishes-complete-fixed-point-test + ;; was removed when demand-bounded evaluation stopped publishing complete + ;; fixed points for point checks (7a3cd3e6). "formal mutation :generated-authority-bypasses-cache-cutover" "formal/smoke/clj/run-verified-authority nonbenchmark"]} diff --git a/formal/counterexamples/EACL-FORMAL-037/entry.edn b/formal/counterexamples/EACL-FORMAL-037/entry.edn index d192619f8..47022c8dc 100644 --- a/formal/counterexamples/EACL-FORMAL-037/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-037/entry.edn @@ -13,6 +13,9 @@ :fix "Add and generation-evict both shared slots in the Datomic schema cache, and make the forced-authority harness require a recursive-routing-certificate call from every backend." :closing-evidence - ["eacl.datomic.impl.indexed-test/indexed-facade-has-no-shared-schema-cache-surface-test" - "eacl.formal.verified-authority-suite/run-nonbenchmark!" - "formal/verification/verified-authority-suites.edn"]} + [;; Historical: eacl.datomic.impl.indexed-test/indexed-facade-has-no-shared-schema-cache-surface-test + ;; asserted only that the deleted names stayed absent. + ;; formal/verification/verified-authority-suites.edn was a generated + ;; evidence ledger, removed in 483911d6. + "eacl.datomic.api-contract-test/generated-authority-is-the-only-production-engine-test" + "eacl.formal.verified-authority-suite/run-nonbenchmark!"]} diff --git a/formal/counterexamples/EACL-FORMAL-039/entry.edn b/formal/counterexamples/EACL-FORMAL-039/entry.edn index d6d016657..64466818c 100644 --- a/formal/counterexamples/EACL-FORMAL-039/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-039/entry.edn @@ -13,8 +13,9 @@ :fix "Pass every materialized path kind through the generated boundary, stream-check exact ordered path-to-edge derivation, and build the host graph and certificate from that same edge vector. Acceptance now proves exact derivation plus exact SCC classification in P+2V+E certified loop iterations." :closing-evidence - ["eacl.formal.production-kernel-test/generated-java-certifies-production-path-to-edge-derivation" - "eacl.formal.production-kernel-test/generated-javascript-certifies-production-path-to-edge-derivation" + [;; Historical: eacl.formal.production-kernel-test/generated-java-certifies-production-path-to-edge-derivation + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). + "eacl.verified-kernel-test/routing-certificate-result-is-bound-to-its-input" "formal mutation :routing-permission-path-omits-dependency-edge" "formal mutation :routing-relation-path-invents-dependency-edge" "formal mutation :routing-path-edge-order-unbound" diff --git a/formal/counterexamples/EACL-FORMAL-040/entry.edn b/formal/counterexamples/EACL-FORMAL-040/entry.edn index 259cb6657..db47001a4 100644 --- a/formal/counterexamples/EACL-FORMAL-040/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-040/entry.edn @@ -15,6 +15,6 @@ :closing-evidence ["eacl.formal.production-kernel-test/production-jvm-two-stream-merge-refines-exact-source-model" "eacl.formal.production-kernel-test/production-javascript-two-stream-merge-refines-exact-source-model" - "eacl.formal.production-kernel-test/optimized-jvm-ordered-merge-refines-generated-chunks" - "eacl.formal.production-kernel-test/optimized-javascript-ordered-merge-refines-generated-chunks" + ;; Historical: eacl.formal.production-kernel-test/optimized-jvm-ordered-merge-refines-generated-chunks + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). "formal/dafny/OrderedMerge.dfy"]} diff --git a/formal/counterexamples/EACL-FORMAL-041/entry.edn b/formal/counterexamples/EACL-FORMAL-041/entry.edn index bc39d57a6..55efb3422 100644 --- a/formal/counterexamples/EACL-FORMAL-041/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-041/entry.edn @@ -13,9 +13,10 @@ :fix "Extend the Dafny advance and leapfrog model with an ordered [side target] reseek trace, prove its length equals the reseek counter and every event carries the exact branch target, expose it through generated Java and JavaScript, compare it with the actual CLJ/CLJS callbacks over all 4,100 campaign cases per runtime, and certify inclusive/exclusive backend scan windows at every materialized fixture EID." :closing-evidence - ["eacl.formal.production-kernel-test/optimized-jvm-leapfrog-intersection-refines-bounded-proof" - "eacl.formal.production-kernel-test/optimized-javascript-leapfrog-intersection-refines-bounded-proof" + [;; Historical: eacl.formal.production-kernel-test/optimized-jvm-leapfrog-intersection-refines-bounded-proof + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). + "eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test" "formal mutations :leapfrog-reseek-wrong-target and :leapfrog-reseek-wrong-side" - "eacl.formal.mutation-control-test/mutation-registry-is-complete-and-killed-test" + "eacl.formal.mutation-control-test/registry-mechanisms-name-and-execute-their-targets-test" "eacl.adapter-certification" "formal/dafny/AcyclicEngine.dfy"]} diff --git a/formal/counterexamples/EACL-FORMAL-042/entry.edn b/formal/counterexamples/EACL-FORMAL-042/entry.edn index 7699a10dc..1c9eff4a8 100644 --- a/formal/counterexamples/EACL-FORMAL-042/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-042/entry.edn @@ -12,7 +12,8 @@ :fix "Return false before singleton/wide selection when the resource-side stream is empty. Model the exact empty/singleton/wide source control in Dafny, prove zero or one intermediate skips direct intersection and the optimized result equals complete far-side evaluation, and compare generated Java/JavaScript Boolean and work traces with actual CLJ/CLJS execution." :closing-evidence - ["eacl.formal.production-kernel-test/generated-java-acyclic-arrow-path-refines-source-control" - "eacl.formal.production-kernel-test/generated-javascript-acyclic-arrow-path-refines-source-control" + [;; Historical: eacl.formal.production-kernel-test/generated-java-acyclic-arrow-path-refines-source-control + ;; and its JavaScript twin were removed with the legacy engine (d96bc4c6). + "eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test" "formal acyclic-arrow source-control mutations" "formal/dafny/AcyclicEngine.dfy"]} diff --git a/formal/counterexamples/EACL-FORMAL-043/entry.edn b/formal/counterexamples/EACL-FORMAL-043/entry.edn index 96d9314d7..9fda6ffaa 100644 --- a/formal/counterexamples/EACL-FORMAL-043/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-043/entry.edn @@ -13,7 +13,7 @@ :fix "Withdraw the false all-root generated-authority claim. Recursive roots execute the generated indexed traversal; certified acyclic roots execute the faster source-specialized host engine with generated routing, page, count, and work decisions plus explicit source-specialization evidence. Keep those assurance classes disjoint in the manifest and regression corpus." :closing-evidence - ["eacl.formal.state-trace-differential-test/generated-decisions-and-source-specialized-acyclic-paths-preserve-order-and-point-locality" - "formal/verification/acyclic-kernel.edn" - "formal/verification/source-specializations.edn" - "formal/verification/indexed-traversal.edn"]} + [;; Historical: formal/verification/acyclic-kernel.edn, + ;; source-specializations.edn and indexed-traversal.edn were generated + ;; evidence ledgers, removed in 483911d6. + "eacl.formal.state-trace-differential-test/generated-decisions-and-source-specialized-acyclic-paths-preserve-order-and-point-locality"]} diff --git a/formal/counterexamples/EACL-FORMAL-045/entry.edn b/formal/counterexamples/EACL-FORMAL-045/entry.edn index 23b4f587e..28f132453 100644 --- a/formal/counterexamples/EACL-FORMAL-045/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-045/entry.edn @@ -19,5 +19,6 @@ "eacl.formal.production-kernel-test" "eacl.formal.state-trace-differential-test" "formal/smoke/clj/run-verified-authority nonbenchmark" - "formal/smoke/cljs/run-verified-authority" - "formal/verification/performance-gates.edn"]} + ;; Historical: formal/verification/performance-gates.edn was a generated + ;; evidence ledger, removed in 483911d6. + "formal/smoke/cljs/run-verified-authority"]} diff --git a/formal/counterexamples/EACL-FORMAL-046/entry.edn b/formal/counterexamples/EACL-FORMAL-046/entry.edn index b6d26b7b6..e466646a0 100644 --- a/formal/counterexamples/EACL-FORMAL-046/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-046/entry.edn @@ -16,6 +16,8 @@ ["formal/dafny/RootDenotation.dfy/EquivalentRuleBodiesHaveEqualSemanticDenotations" "formal/dafny/IndexedRootDenotation.dfy/CertifiedEqualIndexedRootBodiesHaveEqualDenotations" "eacl.engine.stable-discovery-gate-test/fingerprint-is-invariant-under-schema-clause-order-test" - "eacl.engine.stable-discovery-gate-test/independent-oracle-equality-test" - "eacl.bench.subproblem-cache-test/distinct-query-shared-subgraph-cache-benchmark" - "formal/verification/performance-gates.edn"]} + ;; Historical: eacl.bench.subproblem-cache-test/distinct-query-shared-subgraph-cache-benchmark + ;; was retired with the analysis router (3395d961). + ;; formal/verification/performance-gates.edn was a generated evidence + ;; ledger, removed in 483911d6. + "eacl.engine.stable-discovery-gate-test/independent-oracle-equality-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-047/entry.edn b/formal/counterexamples/EACL-FORMAL-047/entry.edn index 3507931a5..d93d99e14 100644 --- a/formal/counterexamples/EACL-FORMAL-047/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-047/entry.edn @@ -16,5 +16,6 @@ ["formal/dafny/PageWindow.dfy/CurrentContinuationRequiresEqualProof" "formal/dafny/PageWindow.dfy/ChangedProofWithoutExactSnapshotIsRejected" "eacl.datascript.keyset-recursion-test/order-perturbing-write-rejects-current-only-cursor-test" - "eacl.datascript.keyset-recursion-test/revoked-boundary-is-stale-test" - "formal/verification/verified-authority-suites.edn"]} + ;; Historical: formal/verification/verified-authority-suites.edn was a + ;; generated evidence ledger, removed in 483911d6. + "eacl.datascript.keyset-recursion-test/revoked-boundary-is-stale-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-048/entry.edn b/formal/counterexamples/EACL-FORMAL-048/entry.edn index 0c3a413fb..185a2478f 100644 --- a/formal/counterexamples/EACL-FORMAL-048/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-048/entry.edn @@ -13,7 +13,9 @@ :fix "Run the routing gate first in the fresh 1 GiB generated-resource JVM, use 40 deterministic warmups and 11 samples per size, and print the complete observation before a failed result throws. The exact P+2V+E logical checks and all allocation/latency ceilings remain unchanged." :closing-evidence - ["eacl.characterization-fixture-test/formal-ci-isolates-and-stops-performance-nrepls-test" + [;; Historical: eacl.characterization-fixture-test/formal-ci-isolates-and-stops-performance-nrepls-test + ;; asserted only the text of formal.yml. "eacl.formal.routing-certificate-benchmark/run-gate!" - ".github/workflows/formal.yml/Gate routing-certificate logical work and JVM allocation" - "formal/verification/performance-gates.edn"]} + ;; Historical: formal/verification/performance-gates.edn was a generated + ;; evidence ledger, removed in 483911d6. + ".github/workflows/formal.yml/Gate routing-certificate logical work and JVM allocation"]} diff --git a/formal/counterexamples/EACL-FORMAL-050/entry.edn b/formal/counterexamples/EACL-FORMAL-050/entry.edn index 659e63690..18683355f 100644 --- a/formal/counterexamples/EACL-FORMAL-050/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-050/entry.edn @@ -13,8 +13,9 @@ :fix "Warm the exact permission-check path for 15,000 calls and gate the median of three independent 5,000-call batch medians. Keep the 1,000 microsecond warm ceiling unchanged. The corrected harness subsequently established the sustained EACL-FORMAL-051 engine regression instead of dismissing it as one transient sample." :closing-evidence - ["eacl.bench.pagination-test/permission-check-benchmark" - ;; Historical: the quantitative-gate fixture test and - ;; formal/verification/performance-gates.edn were superseded by the - ;; executable assurance contract; the recursion gates below remain live. + [;; Historical: eacl.bench.pagination-test/permission-check-benchmark was + ;; retired with the analysis router (3395d961). The quantitative-gate + ;; fixture test and formal/verification/performance-gates.edn were + ;; superseded by the executable assurance contract; the recursion gates + ;; below remain live. "eacl.bench.recursive-performance-gate-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-055/entry.edn b/formal/counterexamples/EACL-FORMAL-055/entry.edn index c3115b7f3..7b57db41f 100644 --- a/formal/counterexamples/EACL-FORMAL-055/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-055/entry.edn @@ -14,6 +14,7 @@ "Anchor every point check at the concrete target. Recursive roots initialize the verified reverse indexed traversal and use its Boolean renderer. Certified acyclic roots use the exact inclusive bound-probe source specialization instead of entering the recursive state machine. Add direction/classification regressions and a 16-versus-1,040 reachable-resource logical/backend-work gate." :closing-evidence ["eacl.formal.state-trace-differential-test/generated-decisions-and-source-specialized-acyclic-paths-preserve-order-and-point-locality" - "eacl.bench.pagination-test/permission-check-benchmark" + ;; Historical: eacl.bench.pagination-test/permission-check-benchmark was + ;; retired with the analysis router (3395d961). "IndexedReverseCompleteness.ExhaustedReverseTraversalRefinesLeastFixedPoint" "IndexedTraversal.ReadRenderResult"]} diff --git a/formal/counterexamples/EACL-FORMAL-056/entry.edn b/formal/counterexamples/EACL-FORMAL-056/entry.edn index 9cf02f846..de488d023 100644 --- a/formal/counterexamples/EACL-FORMAL-056/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-056/entry.edn @@ -13,5 +13,6 @@ :fix "Resolve the generated selection once at execute-page entry and pass that same non-nil selection to both generated pagination decisions. Keep public and direct implementation matrix regressions." :closing-evidence - ["eacl.datascript.impl-test/read-relationships-query-matrix-test" - "eacl.datahike.storage-test/relationship-read-filter-matrix-test"]} + [;; Historical: eacl.datahike.storage-test/relationship-read-filter-matrix-test + ;; was listed here but never committed. + "eacl.datascript.impl-test/read-relationships-query-matrix-test"]} diff --git a/formal/counterexamples/EACL-FORMAL-058/entry.edn b/formal/counterexamples/EACL-FORMAL-058/entry.edn index 555e5f636..40f536683 100644 --- a/formal/counterexamples/EACL-FORMAL-058/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-058/entry.edn @@ -13,5 +13,7 @@ :fix "Remove eager loads of formal-only former-engine namespaces. Let the corpus runner resolve each closing regression lazily only when its evidence namespace is present, and retain a source regression forbidding those eager requires." :closing-evidence - ["eacl.formal.counterexample-replay-test/replay-entrypoint-does-not-eagerly-load-formal-only-oracles-test" + [;; Historical: eacl.formal.counterexample-replay-test/replay-entrypoint-does-not-eagerly-load-formal-only-oracles-test + ;; asserted only the text of bin/formal. + ".github/workflows/formal.yml/Replay minimized counterexample corpus" "EACL_NREPL_PORT= bin/formal counterexample-replay: 42 tests, 2923 assertions, 0 failures/errors"]} diff --git a/formal/counterexamples/EACL-FORMAL-059/entry.edn b/formal/counterexamples/EACL-FORMAL-059/entry.edn index 0063ceb7e..b92b5220e 100644 --- a/formal/counterexamples/EACL-FORMAL-059/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-059/entry.edn @@ -13,7 +13,9 @@ :fix "Make the direct generated-JavaScript page-window smoke construct only the current four-field datatype, leave removed pagination-key rejection to public host-boundary tests, and make the JVM and CLJS recursive-page tests consume one shared cross-runtime expectation." :closing-evidence - ["eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test" + [;; Historical: eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test + ;; asserted only the text of the smoke tests. + "eacl.formal.production-kernel-test/generated-java-drives-production-recursive-pages" "eacl.formal.js-round-trip-test/generated-javascript-page-window-parity" "eacl.formal.production-kernel-test/generated-javascript-drives-production-recursive-pages" "GitHub Actions clean generated-JavaScript differential boundary"]} diff --git a/formal/counterexamples/EACL-FORMAL-060/entry.edn b/formal/counterexamples/EACL-FORMAL-060/entry.edn index efc0b2305..01f4a628a 100644 --- a/formal/counterexamples/EACL-FORMAL-060/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-060/entry.edn @@ -16,4 +16,4 @@ ["RoutingCertificate.SelectEnumerationRoute" "AcyclicEngine.DecideAcyclicPage" "eacl.engine.physical-route-test/exhaustion-count-test" - "eacl.bench.explorer-enumeration-test/explorer-50000-super-user-exact-acyclic-acceptance"]} + "eacl.bench.explorer-enumeration-test/explorer-50000-super-user-exact-count-acceptance"]} diff --git a/formal/counterexamples/EACL-FORMAL-063/entry.edn b/formal/counterexamples/EACL-FORMAL-063/entry.edn index 49fd7b593..c18cf24f2 100644 --- a/formal/counterexamples/EACL-FORMAL-063/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-063/entry.edn @@ -17,6 +17,6 @@ "ExecutionContract.DemandPreservesCertifiedEvaluatorRoute" "ExecutionContract.AcyclicCompletionPreservesCertifiedPublicOrder" "eacl.engine.stable-discovery-gate-test/independent-oracle-equality-test" - "formal/mutations/registry.edn :completed-acyclic-artifact-keeps-fixed-point-order" - "eacl.engine.stable-discovery-gate-test/independent-oracle-equality-test" - "eacl.bench.subproblem-cache-test/distinct-query-shared-subgraph-cache-benchmark"]} + ;; Historical: eacl.bench.subproblem-cache-test/distinct-query-shared-subgraph-cache-benchmark + ;; was retired with the analysis router (3395d961). + "formal/mutations/registry.edn :completed-acyclic-artifact-keeps-fixed-point-order"]} diff --git a/formal/counterexamples/EACL-FORMAL-064/entry.edn b/formal/counterexamples/EACL-FORMAL-064/entry.edn index 50dd8fa17..3e44a3244 100644 --- a/formal/counterexamples/EACL-FORMAL-064/entry.edn +++ b/formal/counterexamples/EACL-FORMAL-064/entry.edn @@ -13,8 +13,8 @@ :fix "Use the supported-writer ordered-generation proof frame. Cursor minting reads only the complete dependency generations and stores the scalar frontier, so unrelated later transactions remain valid without relationship-content scans while relevant writes reject the cursor." :closing-evidence - ["ScalarFrontierCoherence.UnrelatedMutationPreservesFrontier" - "ScalarFrontierCoherence.RelevantMutationAdvancesFrontier" + ["ScalarFrontierCoherence.EqualFrontierHistoryPreservesDependencyStates" + "ScalarFrontierCoherence.StampedDependencySetsTheNewFrontier" "eacl.engine.stable-page-test/page-composition-test" "eacl.engine.stable-page-test/token-rejection-test" - "eacl.bench.explorer-enumeration-test/explorer-10000-user-page-does-not-scale-with-denotation"]} + "eacl.bench.explorer-enumeration-test/explorer-10000-correctness-work-and-latency-gate"]} diff --git a/formal/fixtures/operator-engine/README.md b/formal/fixtures/operator-engine/README.md index 8507331ed..b0cae5f49 100644 --- a/formal/fixtures/operator-engine/README.md +++ b/formal/fixtures/operator-engine/README.md @@ -3,7 +3,7 @@ These inputs are exercised against current code: - `minimized-counterexamples.edn`: `eacl.operator-engine.counterexamples-test` - compares the oracle and intentionally faulty algorithms on retained graphs. + checks the reference oracle on retained graphs that defeated earlier designs. - `union-only-baseline.edn`: `eacl.operator-engine.union-only-baseline-test` captures current public behavior and compares its canonical denotation, order, pagination, and error results with the expected fixture values. diff --git a/formal/fixtures/operator-engine/minimized-counterexamples.edn b/formal/fixtures/operator-engine/minimized-counterexamples.edn index 768e26d1b..15fa811b6 100644 --- a/formal/fixtures/operator-engine/minimized-counterexamples.edn +++ b/formal/fixtures/operator-engine/minimized-counterexamples.edn @@ -11,8 +11,6 @@ {[:folder :p] [:union [:permission :q] [:relation :seed]] [:folder :q] [:intersection [:permission :p] [:relation :eligible]]}} - :evaluation-order [[[:folder :p] [:folder "f"] [:user "alice"]] - [[:folder :q] [:folder "f"] [:user "alice"]]] :query {:permission :q :resource [:folder "f"] :subject [:user "alice"]} :expected true @@ -33,12 +31,6 @@ :expected false :killed-mutant :intersection-grants-on-any-premise} - {:id :partial-right-side-absence - :left :completed-true - :right :incomplete - :expected :propagate-incomplete - :killed-mutant :incomplete-right-treated-as-false} - {:id :swapped-exclusion-operands :snapshot {:objects #{[:user "alice"] [:user "bob"] [:document "d"]} @@ -57,39 +49,6 @@ :expected true :killed-mutant :exclusion-operands-swapped} - {:id :cursor-advanced-through-batch-overread - :page-size 2 - :physical-batch [:a :b :c :d] - :accepted [:a :b :c :d] - :returned [:a :b] - :lookahead-sentinel :c - :expected-cursor-boundary :b - :expected-resume [:c :d] - :killed-mutant :cursor-uses-last-physical-candidate} - - {:id :wrong-typed-id-join-identity - :left #{[:user "same"]} - :right #{[:service "same"]} - :expected #{} - :killed-mutant :join-compares-eid-without-type} - - {:id :incomplete-arrow-object-catalog - :resource [:folder "f"] - :subject [:user "alice"] - :intermediate [:group "g"] - :catalog #{[:folder "f"] [:user "alice"]} - :relationships - #{{:resource [:folder "f"] :relation :parent :subject [:group "g"]} - {:resource [:group "g"] :relation :member :subject [:user "alice"]}} - :expected true - :killed-mutant :arrow-enumerates-incomplete-object-catalog} - - {:id :cache-write-sign-mismatch - :dependencies #{{:relation :banned :sign :negative}} - :changed {:relation :banned :sign :positive} - :expected-invalidated true - :killed-mutant :cache-invalidation-compares-signed-dependency} - {:id :unchecked-scc-certificate :snapshot {:permissions diff --git a/formal/fixtures/performance/task-1.9-dispositions.md b/formal/fixtures/performance/task-1.9-dispositions.md index 54bde6b83..8a8a627ad 100644 --- a/formal/fixtures/performance/task-1.9-dispositions.md +++ b/formal/fixtures/performance/task-1.9-dispositions.md @@ -54,3 +54,7 @@ the negative decision only so it is not silently reintroduced. The red tests are intentional task-1.9 anchors. They must turn green in the owning implementation/spec tasks; weakening or deleting them is not an acceptable resolution. + +`durable-cache-contracts-forbid-request-joining-test` was removed on 2026-10-04, +after the specs it searched stopped requiring flights: it checked the text of +those files, not behavior. diff --git a/formal/smoke/clj/eacl/formal/verified_authority_suite.clj b/formal/smoke/clj/eacl/formal/verified_authority_suite.clj index 1be9985e5..5fbf1628f 100644 --- a/formal/smoke/clj/eacl/formal/verified_authority_suite.clj +++ b/formal/smoke/clj/eacl/formal/verified_authority_suite.clj @@ -43,7 +43,6 @@ eacl.datomic.recursive-cache-test eacl.datomic.schema-basis-test eacl.datomic.schema-test - eacl.datomic.trusted-surface-audit-test eacl.datomic.v8-characterization-test eacl.migrations.v6-to-v7-test eacl.spice-test @@ -53,7 +52,6 @@ eacl.characterization-fixture-test eacl.consistency-test eacl.engine.relationships-test - eacl.formal.cache-strategy-adversarial-test eacl.formal.counterexample-replay-test eacl.formal.dafny-cleanup-gate-test eacl.formal.differential-runner-test diff --git a/formal/smoke/cljs/eacl/formal/verified_authority_test_runner.cljs b/formal/smoke/cljs/eacl/formal/verified_authority_test_runner.cljs index 2672ed30a..d4046247c 100644 --- a/formal/smoke/cljs/eacl/formal/verified_authority_test_runner.cljs +++ b/formal/smoke/cljs/eacl/formal/verified_authority_test_runner.cljs @@ -16,7 +16,6 @@ [eacl.datascript.storage-test] [eacl.engine.relationships-test] [eacl.execution-test] - [eacl.formal.cache-strategy-adversarial-test] [eacl.formal.differential-runner-test] [eacl.formal.generators-test] [eacl.formal.production-kernel-cljs :as production] @@ -131,7 +130,6 @@ 'eacl.secure-format-test 'eacl.subproblem-cache-test 'eacl.verified-kernel-test - 'eacl.formal.cache-strategy-adversarial-test 'eacl.formal.differential-runner-test 'eacl.formal.generators-test 'eacl.datascript.adapter-certification-test diff --git a/modules/eacl-datahike/test/eacl/datahike/adapter_certification_test.clj b/modules/eacl-datahike/test/eacl/datahike/adapter_certification_test.clj index babde65f0..ce821f964 100644 --- a/modules/eacl-datahike/test/eacl/datahike/adapter_certification_test.clj +++ b/modules/eacl-datahike/test/eacl/datahike/adapter_certification_test.clj @@ -125,18 +125,3 @@ (let [second-db-config (:config (d/db second-conn))] (d/release second-conn) (d/delete-database second-db-config)))))) - -(deftest current-db-reference-identity-test - (testing "the exact-basis cache can use immutable DB object identity" - (let [conn (datahike/create-conn) - before-1 (d/db conn) - before-2 (d/db conn) - _ (d/transact conn [{:eacl/id "datahike-reference-identity"}]) - after-1 (d/db conn) - after-2 (d/db conn)] - (is (identical? before-1 before-2) - "an unchanged connection must return the same immutable DB object") - (is (not (identical? before-1 after-1)) - "a committed transaction must replace the immutable DB object") - (is (identical? after-1 after-2) - "the replacement remains stable until the next commit")))) diff --git a/modules/eacl-datahike/test/eacl/datahike/consistency_v3_test.clj b/modules/eacl-datahike/test/eacl/datahike/consistency_v3_test.clj index 8a84b5e07..c77ee524a 100644 --- a/modules/eacl-datahike/test/eacl/datahike/consistency_v3_test.clj +++ b/modules/eacl-datahike/test/eacl/datahike/consistency_v3_test.clj @@ -370,7 +370,6 @@ after (datahike/cache-stats authorization)] (is (= [(second documents)] (:data historical-1))) (is (= (:data historical-1) (:data historical-2))) - (is (nil? (get-in historical-1 [:page-info :cursor-recovery]))) (is (true? (:cached? historical-1))) (is (true? (:cached? historical-2))) (is (= (:bypasses before) (:bypasses after)) @@ -567,11 +566,6 @@ (is (not (source/supports? basis-source :snapshots :durable-history))) (is (not (source/supports? basis-source :snapshots :conditional-exact))))) -(deftest raw-db-entry-points-are-removed-test - (is (nil? (ns-resolve 'eacl.datahike.core 'datahike-can?))) - (is (nil? (ns-resolve 'eacl.datahike.core - 'datahike-read-relationships)))) - (deftest reader-branch-and-merge-metadata-test (let [writer-conn (datahike/create-conn) config (:config (d/db writer-conn)) @@ -800,7 +794,6 @@ (get-in page-2 [:page-info :end-cursor]) (:runtime authorization))] (is (= [(second relationships)] (:data page-2))) - (is (nil? (get-in page-2 [:page-info :cursor-recovery]))) (is (= (get-in cursor-data [:graph-head :exact-locator]) (get-in exact-cursor-data [:graph-head :exact-locator]))))) (let [fresh-page-1 @@ -817,8 +810,7 @@ (eacl/read-relationships authorization (assoc query :after fresh-cursor))] - (is (= [(second relationships)] (:data page))) - (is (nil? (get-in page [:page-info :cursor-recovery]))))) + (is (= [(second relationships)] (:data page))))) (testing "a changed consistency contract is a different query scope" (is (= :eacl.pagination/invalid-cursor (:type diff --git a/modules/eacl-datahike/test/eacl/datahike/contract_test.clj b/modules/eacl-datahike/test/eacl/datahike/contract_test.clj index 56a6469b5..18296de9f 100644 --- a/modules/eacl-datahike/test/eacl/datahike/contract_test.clj +++ b/modules/eacl-datahike/test/eacl/datahike/contract_test.clj @@ -57,7 +57,6 @@ (is (> (datahike/cache-content-revision client) before)))) (deftest native-speculative-contract-test - (is (nil? (ns-resolve 'eacl.datahike.core 'snapshot))) (let [conn (datahike/create-conn nil {}) config (:config (d/db conn)) client (datahike/make-client conn {})] diff --git a/modules/eacl-datahike/test/eacl/datahike/storage_test.clj b/modules/eacl-datahike/test/eacl/datahike/storage_test.clj index 2a89e0f70..01f530f32 100644 --- a/modules/eacl-datahike/test/eacl/datahike/storage_test.clj +++ b/modules/eacl-datahike/test/eacl/datahike/storage_test.clj @@ -1,6 +1,5 @@ (ns eacl.datahike.storage-test - (:require [clojure.set] - [clojure.test :refer [deftest is testing]] + (:require [clojure.test :refer [deftest is testing]] [datahike.api :as d] [eacl.core :as eacl] [eacl.datahike.core :as datahike] @@ -67,13 +66,6 @@ {"attributes as keywords" false "attributes as numeric refs" true}) -(deftest derived-expression-metrics-are-not-schema-attributes-test - (let [idents (set (map :db/ident schema/datahike-schema))] - (is (empty? - (clojure.set/intersection - idents - expression-persistence/retired-expression-attributes))))) - (defn- exception-data [thunk] (try (thunk) diff --git a/modules/eacl-datahike/test/eacl/operator_engine/experiments_test.clj b/modules/eacl-datahike/test/eacl/operator_engine/experiments_test.clj deleted file mode 100644 index 70f3f1f0d..000000000 --- a/modules/eacl-datahike/test/eacl/operator_engine/experiments_test.clj +++ /dev/null @@ -1,82 +0,0 @@ -(ns eacl.operator-engine.experiments-test - (:require [clojure.test :refer [deftest is]] - [eacl.operator-engine.experiments :as experiments])) - -(deftest deterministic-operator-experiments-self-check-test - (let [summary - (experiments/run-deterministic - {:cover-trials 2000 - :anchor-trials 500 - :recursive-anchor-trials 250})] - (is (true? (get-in summary [:cover :passed?]))) - (is (zero? (get-in summary [:anchor-gated :result-failures]))) - (is (< (get-in summary [:anchor-gated :anchor-gated-states]) - (get-in summary [:anchor-gated :any-child-states]))) - (is (zero? (get-in summary - [:recursive-anchor-gated :result-failures]))) - (is (zero? (get-in summary - [:recursive-anchor-gated - :arrival-order-failures]))) - (is (zero? (get-in summary - [:recursive-anchor-gated - :retained-state-failures]))) - (is (< (get-in summary - [:recursive-anchor-gated :anchor-parent-slots]) - (get-in summary - [:recursive-anchor-gated :any-child-parent-slots]))) - (is (= 21 (get-in summary - [:adaptive-batching :all-accepted :adaptive - :physical-candidates]))) - (is (= 256 (get-in summary - [:adaptive-batching :all-accepted :fixed-width - :physical-candidates]))) - (is (= (range 0 21000 1000) - (get-in summary [:leapfrog :leapfrog :results]))) - (is (zero? (get-in summary - [:k-way-leapfrog :random-result-failures]))) - (is (zero? (get-in summary - [:k-way-leapfrog :random-bound-failures]))) - (is (= {:anchor-rounds 0 - :driver-lower-bound-seeks 0 - :operand-lower-bound-seeks 0 - :lower-bound-comparisons 0 - :accepted 0} - (get-in summary [:k-way-leapfrog :zero-demand]))) - (is (= {:anchor-rounds 1 - :driver-lower-bound-seeks 0 - :operand-lower-bound-seeks 1 - :lower-bound-comparisons 1 - :accepted 0} - (get-in summary [:k-way-leapfrog :early-exhaustion]))) - (is (true? (get-in summary - [:k-way-leapfrog :adversarial :equal-results?]))) - (is (< (get-in summary - [:k-way-leapfrog :adversarial :k-way - :anchor-rounds]) - (get-in summary - [:k-way-leapfrog :adversarial :sequential-binary - :head-comparisons]))) - (is (= 21 (get-in summary - [:k-way-leapfrog :adversarial :bounded-k-way - :accepted]))) - (is (= (range 0 21000 1000) - (get-in summary - [:k-way-leapfrog :adversarial :bounded-k-way - :results]))) - (is (= 20000 (get-in summary [:memoization :saved-leaf-probes]))))) - -(deftest strategy-matrix-covers-dimensional-performance-risks-test - (let [summary (experiments/strategy-matrix-experiment)] - (is (= 108 (:intersection-cases summary))) - (is (= 12 (:exclusion-cases summary))) - (is (true? (get-in summary [:acceptance :no-eager-selection]))) - (is (true? (get-in summary - [:acceptance :all-adaptive-bounded?]))) - (is (true? (get-in summary - [:acceptance :warm-physical-predicates-zero?]))) - (is (every? #(<= (get-in % [:leapfrog-galloping :accepted]) - (get-in % [:dimensions :page-demand])) - (:intersections summary))) - (is (every? #(<= (get-in % [:anti-join :accepted]) - (get-in % [:dimensions :page-demand])) - (:exclusions summary))))) diff --git a/modules/eacl-datalevin/test/eacl/datalevin/expression_storage_test.clj b/modules/eacl-datalevin/test/eacl/datalevin/expression_storage_test.clj index d1a7ab691..697153d97 100644 --- a/modules/eacl-datalevin/test/eacl/datalevin/expression_storage_test.clj +++ b/modules/eacl-datalevin/test/eacl/datalevin/expression_storage_test.clj @@ -61,10 +61,6 @@ :source-lifecycle #uuid "77ced691-3afb-564f-93a0-92173b63969e" :security-key test-key})) -(deftest derived-expression-metrics-are-not-schema-attributes-test - (is (every? #(not (contains? schema/datalevin-schema %)) - expression-persistence/retired-expression-attributes))) - (defn- exception-data [thunk] (try (thunk) diff --git a/modules/eacl-datascript/test/eacl/baseline/baseline_test.clj b/modules/eacl-datascript/test/eacl/baseline/baseline_test.clj index cb7e7ad21..702b2b95b 100644 --- a/modules/eacl-datascript/test/eacl/baseline/baseline_test.clj +++ b/modules/eacl-datascript/test/eacl/baseline/baseline_test.clj @@ -50,13 +50,8 @@ (str "missing frozen snapshot for " fixture-key " — run (eacl.baseline.capture/capture-all!)")) (when frozen - (is (= (comparable frozen) (comparable fresh)))))))) - -(deftest baseline-invariants-test - (doseq [fixture-key (keys capture/fixtures)] - (testing (str fixture-key) - (let [{:keys [forward]} (capture/read-snapshot fixture-key)] - (doseq [[principal-key result] forward] + (is (= (comparable frozen) (comparable fresh)))) + (doseq [[principal-key result] (:forward fresh)] (testing (str principal-key) (is (true? (:page-composition-equals-one-shot? result))) (is (true? (:duplicate-free? result))) diff --git a/modules/eacl-datascript/test/eacl/datascript/cljs_test_runner.cljs b/modules/eacl-datascript/test/eacl/datascript/cljs_test_runner.cljs index e646deef5..a49705aa2 100644 --- a/modules/eacl-datascript/test/eacl/datascript/cljs_test_runner.cljs +++ b/modules/eacl-datascript/test/eacl/datascript/cljs_test_runner.cljs @@ -110,7 +110,6 @@ [eacl.spicedb.resource-bounds-test] [eacl.subproblem-cache-test] [eacl.verified-kernel-test] - [eacl.formal.cache-strategy-adversarial-test] [eacl.formal.differential-runner-test] [eacl.formal.executed-mutation-controls] [eacl.formal.generators-test] @@ -256,7 +255,6 @@ 'eacl.spicedb.resource-bounds-test 'eacl.subproblem-cache-test 'eacl.verified-kernel-test - 'eacl.formal.cache-strategy-adversarial-test 'eacl.formal.differential-runner-test 'eacl.formal.executed-mutation-controls 'eacl.formal.generators-test diff --git a/modules/eacl-datascript/test/eacl/datascript/consistency_v3_test.cljc b/modules/eacl-datascript/test/eacl/datascript/consistency_v3_test.cljc index 20849eced..4cde722bc 100644 --- a/modules/eacl-datascript/test/eacl/datascript/consistency_v3_test.cljc +++ b/modules/eacl-datascript/test/eacl/datascript/consistency_v3_test.cljc @@ -313,7 +313,6 @@ (is (= :eacl.pagination/stale-cursor (:type recovered-page-2))) (do (is (= [(second documents)] (:data recovered-page-2))) - (is (nil? (get-in recovered-page-2 [:page-info :cursor-recovery]))) (is (true? (:cached? recovered-page-2)))))) (testing "a newly signed cursor for the same boundary also reuses it" (is (not= @@ -473,12 +472,6 @@ (is (= before after) "unsupported exact selection must fail before cache access"))) -#?(:clj - (deftest raw-db-entry-points-are-removed-test - (is (nil? (ns-resolve 'eacl.datascript.core 'datascript-can?))) - (is (nil? (ns-resolve 'eacl.datascript.core - 'datascript-read-relationships))))) - (deftest cloned-connections-are-distinct-sources-and-listener-independent-test (let [original-listen! ds/listen! conn (datascript/create-conn) diff --git a/modules/eacl-datascript/test/eacl/datascript/contract_test.cljc b/modules/eacl-datascript/test/eacl/datascript/contract_test.cljc index a1f9ae917..c7df57c04 100644 --- a/modules/eacl-datascript/test/eacl/datascript/contract_test.cljc +++ b/modules/eacl-datascript/test/eacl/datascript/contract_test.cljc @@ -14,7 +14,6 @@ [eacl.cursor :as cursor] [eacl.datascript.core :as datascript] [eacl.datascript.schema :as schema] - [eacl.engine.v8 :as engine] [eacl.execution :as execution] [eacl.proof-frame :as proof-frame] [eacl.relay :as relay] @@ -26,10 +25,6 @@ (defrecord CursorRecordId [value]) (deftest native-speculative-contract-test - #?(:clj - (is (nil? (ns-resolve 'eacl.datascript.core 'snapshot))) - :cljs - (is true)) (let [conn (datascript/create-conn) client (datascript/make-client conn {})] (contract/assert-speculative-contract! @@ -415,42 +410,6 @@ (is (= :eacl/invalid-config (:type error))) (is (= [:engine-selection] (:unknown-keys error))))) -(deftest raw-retraction-requires-explicit-cache-expiry-test - (let [conn (datascript/create-conn) - client (datascript/make-client conn {}) - user (eacl/spice-object :user "raw-write-user") - document (eacl/spice-object :document "raw-write-doc")] - (eacl/write-schema! - client - "definition user {} - definition document { - relation owner: user - permission view = owner - }") - (ds/transact! conn [{:eacl/id (:id user)} - {:eacl/id (:id document)}]) - (eacl/create-relationship! - client (eacl/->Relationship user :owner document)) - (is (true? (eacl/can? client user :view document))) - (is (true? (eacl/can? client user :view document)) - "the repeated identical check is served from the cache") - ;; Retract the relationship tuples OUTSIDE every EACL writer. - (let [db (ds/db conn) - retractions - (into [] - (mapcat - (fn [attribute] - (map (fn [datom] - [:db/retract (:e datom) attribute (:v datom)]) - (ds/datoms db :aevt attribute)))) - [relationship-storage/forward-attribute - relationship-storage/reverse-attribute])] - (is (seq retractions)) - (ds/transact! conn retractions)) - (datascript/expire-cache! client) - (is (false? (eacl/can? client user :view document)) - "unsupported raw mutation is safe after every affected client expires"))) - (deftest unsupported-mutation-recovery-requires-every-client-and-data-repair-test (let [conn (datascript/create-conn) client-a (datascript/make-client conn {}) @@ -1145,8 +1104,8 @@ [:tree-root :intermediate :children 0 :leaf :subjects]))) "a numeric public permission-tree root must pass through the public codec")))) -(deftest rendered-keys-copy-caller-owned-query-containers-test - #?(:clj +#?(:clj + (deftest rendered-keys-copy-caller-owned-query-containers-test (let [conn (datascript/create-conn) client (datascript/make-client @@ -1193,12 +1152,10 @@ (is (not-any? #(identical? query %) reachable)) (is (not-any? #(instance? clojure.lang.PersistentTreeMap %) reachable) - "the Caffeine key cannot retain the caller's comparator closure"))) - :cljs - (is true))) + "the Caffeine key cannot retain the caller's comparator closure"))))) -(deftest integer-representations-cannot-alias-cursor-authority-test - #?(:clj +#?(:clj + (deftest integer-representations-cannot-alias-cursor-authority-test (let [conn (datascript/create-conn) client (datascript/make-client @@ -1260,12 +1217,10 @@ (ex-data thrown)))] (is (= [long-document] (:data long-page))) (is (= :eacl.pagination/unsupported-cursor-identity (:type error))) - (is (= :query (:position error))))) - :cljs - (is true))) + (is (= :query (:position error))))))) -(deftest noncanonical-permission-tree-root-identities-do-not-alias-test - #?(:clj +#?(:clj + (deftest noncanonical-permission-tree-root-identities-do-not-alias-test (let [conn (datascript/create-conn) client (datascript/make-client @@ -1303,9 +1258,7 @@ client alice :reader stored-vector) (is (= [alice] (tree-subjects ["same"]))) (is (empty? (tree-subjects '("same"))) - "equal host values distinguished by the codec must not share a completed tree")) - :cljs - (is true))) + "equal host values distinguished by the codec must not share a completed tree")))) (deftest metadata-sensitive-identities-cannot-alias-page-cursors-test (let [conn (datascript/create-conn) @@ -1653,23 +1606,30 @@ (eacl/create-relationships! client [(eacl/->Relationship other-user :owner document-2)]) + ;; A permission's plan is sealed once per schema generation whatever + ;; the cache mode, so seal read_b's before comparing the two modes. + (is (true? (decision user :read_b server-1 false))) (let [cached-work (atom {}) bypass-work (atom {}) cached-allowed? - (binding [engine/*backend-work-stats* cached-work] + (binding [backend/*backend-op-stats* cached-work] (decision user :read_b server-1 true)) bypass-allowed? - (binding [engine/*backend-work-stats* bypass-work] - (decision user :read_b server-1 false)) - after (datascript/cache-stats client)] + (binding [backend/*backend-op-stats* bypass-work] + (decision user :read_b server-1 false))] (is (true? cached-allowed?)) (is (= cached-allowed? bypass-allowed?)) - (is (= (:executed-backend-operations @bypass-work) - (:executed-backend-operations @cached-work)) - "a cold demand cache attempt performs the same semantic work as bypass") - (is (not (contains? (:subproblems after) - :managed-projection-hits)) - "demand mode has no shared partial-projection cache"))) + (is (pos? (get @bypass-work :subject->resources 0)) + "the bypass scans the backend") + (is (= (if orchestration/*qualified-authorization-enabled?* + @bypass-work + ;; Under the legacy binding one proof-frame read lets the + ;; attempt reuse read_a's team scan across the unrelated write. + (-> @bypass-work + (dissoc :resource->subjects) + (assoc :proof-frame 1))) + @cached-work) + "a cold demand cache attempt adds no scan to the bypass's work"))) ;; A write to the depended-on relation must select a different managed key, ;; not reuse the previous negative projection. diff --git a/modules/eacl-datascript/test/eacl/datascript/keyset_recursion_test.clj b/modules/eacl-datascript/test/eacl/datascript/keyset_recursion_test.clj index d35d99b92..c85b3c48e 100644 --- a/modules/eacl-datascript/test/eacl/datascript/keyset_recursion_test.clj +++ b/modules/eacl-datascript/test/eacl/datascript/keyset_recursion_test.clj @@ -85,7 +85,6 @@ (if orchestration/*qualified-authorization-enabled?* (is (= :eacl.pagination/stale-cursor (:type (error-data #(lookup client request))))) (let [page-2 (lookup client request)] - (is (nil? (get-in page-2 [:page-info :cursor-recovery]))) (is (empty? (set/intersection (set (page-ids page-1)) (set (page-ids page-2))))))))) (deftest bare-last-requires-explicit-completion-and-preserves-logical-order-test diff --git a/modules/eacl-datascript/test/eacl/datascript/snapshot_lifecycle_test.cljc b/modules/eacl-datascript/test/eacl/datascript/snapshot_lifecycle_test.cljc index b45e8b8a7..f2b7f6ebe 100644 --- a/modules/eacl-datascript/test/eacl/datascript/snapshot_lifecycle_test.cljc +++ b/modules/eacl-datascript/test/eacl/datascript/snapshot_lifecycle_test.cljc @@ -328,10 +328,6 @@ (is (empty? (:provider-calls failure))))) (deftest raw-database-snapshot-constructor-is-not-public-test - #?(:clj - (is (nil? (ns-resolve 'eacl.datascript.core 'snapshot))) - :cljs - (is true)) (let [{:keys [conn]} (fixture) other-conn (datascript/create-conn) cases @@ -1394,43 +1390,6 @@ (is (= 1 (:release! provider-calls 0))) (is (= 1 db-calls)))) -(deftest selected-snapshot-releases-when-context-construction-fails-test - (let [{:keys [conn client user account]} (fixture) - error (atom nil) - {:keys [provider-calls db-calls]} - (with-redefs - [execution/check! - (fn - ([stage] - (when (= :consistency-selected stage) - (throw - (ex-info "injected context failure" - {:type :test/context-construction})))) - ([contract stage] - (if (= :consistency-selected stage) - (throw - (ex-info "injected context failure" - {:type :test/context-construction})) - nil)) - ([contract stage consumed-work] - (if (= :consistency-selected stage) - (throw - (ex-info "injected context failure" - {:type :test/context-construction})) - nil)))] - (observed-call - conn - #(try - (eacl/can? client user :admin account) - (catch #?(:clj clojure.lang.ExceptionInfo - :cljs cljs.core.ExceptionInfo) - failure - (reset! error (ex-data failure))))))] - (is (= :test/context-construction (:type @error))) - (is (= 1 (:acquire-current! provider-calls 0))) - (is (= 1 (:release! provider-calls 0))) - (is (= 1 db-calls)))) - (defn- observed-failure [conn f] (let [failure (atom nil) diff --git a/modules/eacl-datascript/test/eacl/datascript/storage_test.cljc b/modules/eacl-datascript/test/eacl/datascript/storage_test.cljc index d8cabb512..cc477a96c 100644 --- a/modules/eacl-datascript/test/eacl/datascript/storage_test.cljc +++ b/modules/eacl-datascript/test/eacl/datascript/storage_test.cljc @@ -214,10 +214,6 @@ (is (every? #(not (contains? schema/datascript-schema %)) removed-attributes)))) -(deftest derived-expression-metrics-are-not-schema-attributes-test - (is (every? #(not (contains? schema/datascript-schema %)) - expression-persistence/retired-expression-attributes))) - (deftest full-arity-index-boundaries-test (let [conn (schema/create-conn) _ (ds/transact! conn [{:eacl/id "subject-a"} diff --git a/modules/eacl-datascript/test/eacl/engine/continuation_reuse_test.cljc b/modules/eacl-datascript/test/eacl/engine/continuation_reuse_test.cljc index a330948e7..312199eb2 100644 --- a/modules/eacl-datascript/test/eacl/engine/continuation_reuse_test.cljc +++ b/modules/eacl-datascript/test/eacl/engine/continuation_reuse_test.cljc @@ -504,15 +504,6 @@ (is (identical? plan-1 plan-2) "re-wrapping the source at another basis must hit the plan registry"))) -(deftest default-lifecycle-is-the-portable-cross-process-constant-test - (let [{client-a :client} (seed-fixture-client! - (fixture-for :explorer-acyclic)) - {client-r :client} (seed-fixture-client! - (fixture-for :explorer-recursive))] - (is (= #uuid "00000000-0000-0000-0000-000000000000" - (get-in client-a [:runtime :source-lifecycle]) - (get-in client-r [:runtime :source-lifecycle]))))) - (deftest checkpoint-store-adopts-client-context-test (let [{:keys [conn]} (seed-fixture-client! (fixture-for :explorer-acyclic)) diff --git a/modules/eacl-datascript/test/eacl/engine/stable_reducer_test.cljc b/modules/eacl-datascript/test/eacl/engine/stable_reducer_test.cljc index bcdf7d07e..0e665fd8e 100644 --- a/modules/eacl-datascript/test/eacl/engine/stable_reducer_test.cljc +++ b/modules/eacl-datascript/test/eacl/engine/stable_reducer_test.cljc @@ -339,7 +339,6 @@ (catch #?(:clj clojure.lang.ExceptionInfo :cljs cljs.core.ExceptionInfo) error (is (= :max-admissions (:limit (ex-data error)))) - (is (= [:sentinel] (:stack state))) (is (empty? (persistent! (:admitted state))))))))] (assert-unchanged! [(item 1)]) (assert-unchanged! [(item 1) (item 2)]))) diff --git a/modules/eacl-datascript/test/eacl/operator/recursive_test.cljc b/modules/eacl-datascript/test/eacl/operator/recursive_test.cljc index 3db2d0d7f..cc0f187cd 100644 --- a/modules/eacl-datascript/test/eacl/operator/recursive_test.cljc +++ b/modules/eacl-datascript/test/eacl/operator/recursive_test.cljc @@ -795,23 +795,6 @@ (defn- page-ids [page] (mapv :id (:data page))) -(deftest public-recursive-operator-routing-can-be-disabled-test - (let [{:keys [public-adapter]} (chain-fixture) - alice (public-object :user "alice") - f0 (public-object :folder "f0")] - (binding [engine/*operator-routing-enabled?* false] - (is (= :eacl.operator/routing-disabled - (:type - (error-data - #(engine/can? public-adapter alice :allowed f0))))) - (is (= :eacl.operator/routing-disabled - (:type - (error-data - #(engine/lookup-resources - public-adapter - {:subject alice :permission :allowed - :resource/type :folder :first 1})))))))) - (deftest public-recursive-operator-operation-matrix-is-exact-test (let [{:keys [public-adapter alice bob f0 f1 f2 eid]} (chain-fixture) public-alice (public-object :user "alice") diff --git a/modules/eacl-datascript/test/eacl/performance/amplification_reproduction.clj b/modules/eacl-datascript/test/eacl/performance/amplification_reproduction.clj index 2c92e0fdc..5580aa993 100644 --- a/modules/eacl-datascript/test/eacl/performance/amplification_reproduction.clj +++ b/modules/eacl-datascript/test/eacl/performance/amplification_reproduction.clj @@ -27,8 +27,7 @@ [eacl.request.counters :as request-counters] [eacl.schema.errors :as schema-errors] [eacl.schema.expression-persistence :as expression-persistence] - [eacl.subproblem-cache :as subproblem] - [eacl.test-support.repo :as repo])) + [eacl.subproblem-cache :as subproblem])) (def source-base "e137dc55512d4eeebcc31cfbe5087d61ab04465b") (def classpath-sha256 @@ -1005,30 +1004,6 @@ (not (:cached? current-cold)) (:cached? current-hit))})) -(defn cache-flight-contract-probe - [] - (let [specs - ["openspec/specs/single-flight-coordination/spec.md" - "openspec/specs/answer-cache-bounding/spec.md" - "openspec/specs/verified-subproblem-cache/spec.md"] - positive-pattern - #"(?i)joins that flight|must wait or reject|inheriting[^\n]*single-flight coordination|registered flights|single-flight waits" - observations - (mapv - (fn [path] - (let [file (repo/file path) - text (when (.isFile file) (slurp file)) - matches (when text (re-seq positive-pattern text))] - {:path path - :exists? (.isFile file) - :positive-flight-requirements (count matches)})) - specs)] - {:observations observations - :positive-flight-requirements - (reduce + 0 (map :positive-flight-requirements observations)) - :reconciled? - (zero? (reduce + 0 (map :positive-flight-requirements observations)))})) - (def ^:private rejection-scan-schema "definition user {} definition document { diff --git a/modules/eacl-datascript/test/eacl/performance/correctness_gate_test.clj b/modules/eacl-datascript/test/eacl/performance/correctness_gate_test.clj index a141c0952..756addd10 100644 --- a/modules/eacl-datascript/test/eacl/performance/correctness_gate_test.clj +++ b/modules/eacl-datascript/test/eacl/performance/correctness_gate_test.clj @@ -23,9 +23,3 @@ (is (:incompatible-entry-missed? observation) (str "pre-rollout answer survived compatibility change: " observation)))) - -(deftest durable-cache-contracts-forbid-request-joining-test - (let [observation (reproduction/cache-flight-contract-probe)] - (is (:reconciled? observation) - (str "positive flight/join requirements remain: " - (:observations observation))))) diff --git a/modules/eacl-datomic/test/eacl/bench/pagination_test.clj b/modules/eacl-datomic/test/eacl/bench/pagination_test.clj index 1f324edca..d91fcf95f 100644 --- a/modules/eacl-datomic/test/eacl/bench/pagination_test.clj +++ b/modules/eacl-datomic/test/eacl/bench/pagination_test.clj @@ -15,7 +15,6 @@ [eacl.datomic.core :as spiceomic] [eacl.datomic.db :as ddb] [eacl.datomic.impl :as impl :refer [Relationship]] - [eacl.datomic.impl.indexed :as impl.indexed] [eacl.datomic.schema :as schema] [eacl.engine.stable-page :as stable-page] [eacl.engine.v8 :as engine] @@ -234,7 +233,7 @@ (let [stats (atom {}) start (System/nanoTime) {:keys [ids pages]} - (binding [impl.indexed/*recursive-traversal-stats* stats] + (binding [engine/*recursive-traversal-stats* stats] (loop [after nil ids [] pages 0] diff --git a/modules/eacl-datomic/test/eacl/datomic/adversarial_v8_review_test.clj b/modules/eacl-datomic/test/eacl/datomic/adversarial_v8_review_test.clj index 28500679b..810700573 100644 --- a/modules/eacl-datomic/test/eacl/datomic/adversarial_v8_review_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/adversarial_v8_review_test.clj @@ -75,59 +75,6 @@ :request {:subject subject :resource resource :permission :view :caveat-context {"flag" false} :cache? false}}))) -(deftest safe-retraction-must-not-weaken-a-caveat-into-expiry-only - (with-review-client - qualified-schema - (fn [conn client] - (let [{:keys [caveat-eid qualifier-eid request]} (seed-qualified! conn client) - before (d/db conn) - before-result (eacl/check-permission client request)] - (is (some? caveat-eid)) - (is (some? qualifier-eid)) - (is (= :no-permission (:permissionship before-result))) - (let [outcome (retract-outcome! conn caveat-eid) - after (d/db conn) - after-result (eacl/check-permission client request)] - (is (:error outcome) "Caveat definitions are not object-deletion targets") - (is (contains? (:reasons outcome) :protected-control-entity)) - (is (= (d/basis-t before) (d/basis-t after)) - "a rejected deletion must not commit any ref cleanup") - (is (= caveat-eid (d/entid after [:eacl.caveat/name "enabled"]))) - (is (= :no-permission (:permissionship after-result)) - (str "Native result after attempted deletion: " (pr-str after-result)))))))) - -(deftest safe-retraction-must-reject-qualifier-entity-targets - (with-review-client - qualified-schema - (fn [conn client] - (let [{:keys [qualifier-eid]} (seed-qualified! conn client) - before (d/db conn) - outcome (retract-outcome! conn qualifier-eid)] - (is (:error outcome)) - (is (contains? (:reasons outcome) :protected-control-entity)) - (is (= (d/basis-t before) (d/basis-t (d/db conn)))) - (is (seq (d/datoms (d/db conn) :eavt qualifier-eid))))))) - -(deftest component-closure-must-not-delete-a-caveat-definition - (with-review-client - qualified-schema - (fn [conn client] - (let [{:keys [caveat-eid request]} (seed-qualified! conn client)] - @(d/transact conn [{:db/ident :review/component - :db/valueType :db.type/ref - :db/cardinality :db.cardinality/one - :db/isComponent true}]) - @(d/transact conn [{:eacl/id "review/parent" - :review/component caveat-eid}]) - (let [before (d/db conn) - outcome (retract-outcome! conn [:eacl/id "review/parent"])] - (is (:error outcome)) - (is (contains? (:reasons outcome) :protected-control-entity)) - (is (= (d/basis-t before) (d/basis-t (d/db conn)))) - (is (some? (d/entid (d/db conn) [:eacl/id "review/parent"]))) - (is (= :no-permission - (:permissionship (eacl/check-permission client request))))))))) - (defn relation-id [db name] (d/entid db [:eacl.relation/resource-type+relation-name+subject-type [:node name :node]])) diff --git a/modules/eacl-datomic/test/eacl/datomic/api_contract_test.clj b/modules/eacl-datomic/test/eacl/datomic/api_contract_test.clj index d1db6b76b..d56e56195 100644 --- a/modules/eacl-datomic/test/eacl/datomic/api_contract_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/api_contract_test.clj @@ -352,17 +352,6 @@ (:eacl/error (ex-data-of #(eacl/lookup-resources tight query))))) (is (= 10 (count (:data (eacl/lookup-resources roomy query))))))) - (testing "a partial override keeps the other defaults instead of disabling them" - (let [client (core/make-client conn {:recursive-traversal-limits {:max-derived-grants 3}})] - (is (= :eacl.recursive-traversal/limit-exceeded - (:eacl/error (ex-data-of #(eacl/lookup-resources - client - {:subject (spice-object :user "u") - :permission :read - :resource/type :folder - :first 10 - :evaluation :complete-denotation}))))))) - (testing "a malformed limits map is rejected at construction" (doseq [bad [{:no-such-limit 1} {:max-derived-grants 0} {:max-derived-grants "many"} :not-a-map]] (is (= :eacl/invalid-config diff --git a/modules/eacl-datomic/test/eacl/datomic/cache_differential_test.clj b/modules/eacl-datomic/test/eacl/datomic/cache_differential_test.clj index 2afb3f04e..100581437 100644 --- a/modules/eacl-datomic/test/eacl/datomic/cache_differential_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/cache_differential_test.clj @@ -18,7 +18,6 @@ [eacl.core :as eacl :refer [->Relationship spice-object]] [eacl.datomic.core :as core] [eacl.datomic.datomic-helpers :refer [with-mem-conn]] - [eacl.datomic.impl.indexed :as idx] [eacl.datomic.schema :as schema] [eacl.engine.v8 :as engine])) @@ -222,7 +221,7 @@ ;; stale cache at all. That gap matters now that exact-result entries are keyed ;; by per-relation stamps: an answer stays cached until a relation in ITS ;; dependency set is written, and the dependency set comes from -;; idx/permission-relationship-eids walking the permission graph. If that walk +;; engine/permission-relationship-eids walking the permission graph. If that walk ;; ever misses a relation — an arrow target, a nested self-permission, a ;; recursive back-edge — the epoch will not move for a write that changes the ;; answer, and the cache serves a revoked grant. @@ -334,7 +333,9 @@ ;; caller-supplied providers can neither inject nor share these values. (with-mem-conn [conn schema/v8-schema] (let [boot (client conn {:cache shared-cache/no-cache}) - _ (seed-acyclic! conn boot 12) + ;; Large enough that replaying the walk from its start costs more + ;; than the ceiling below; a shorter walk cannot tell the two apart. + _ (seed-acyclic! conn boot 24) acl (client conn {}) oracle (client conn {:cache shared-cache/no-cache}) query {:subject (spice-object :user "alice") @@ -345,13 +346,13 @@ cursor-1 (get-in page-1 [:page-info :end-cursor]) page-2-stats (atom {}) page-2 - (binding [idx/*recursive-traversal-stats* page-2-stats] + (binding [engine/*recursive-traversal-stats* page-2-stats] (eacl/lookup-resources acl (assoc query :first 3 :after cursor-1))) cursor-2 (get-in page-2 [:page-info :end-cursor]) page-3-stats (atom {}) page-3 - (binding [idx/*recursive-traversal-stats* page-3-stats] + (binding [engine/*recursive-traversal-stats* page-3-stats] (eacl/lookup-resources acl (assoc query :first 3 :after cursor-2)))] ;; Order ABI v2 (acyclic-keyset-pagination): an acyclic root's @@ -367,15 +368,22 @@ "keyset pages consult no client-scoped checkpoint") (is (= 0 (:continuation-hits @page-3-stats 0)) "later pages remain stateless") + (is (pos? (:advanced-datoms @page-2-stats 0)) + "the observer sees the page's own scans") (let [reference (max 1 (:advanced-datoms @page-2-stats 0) (:advanced-datoms @page-3-stats 0)) - ceiling (+ 10 (* 4 reference))] + ceiling (+ 10 (* 4 reference)) + replay-stats (atom {})] + (binding [engine/*recursive-traversal-stats* replay-stats] + (eacl/lookup-resources oracle (assoc query :first 1000))) + (is (< ceiling (:advanced-datoms @replay-stats 0)) + "deriving the walk from its start costs more than the ceiling allows one page") (loop [after (get-in page-3 [:page-info :end-cursor]) k 4] (is (< k 20) "walk terminates") (when (and after (< k 20)) (let [stats (atom {}) - page (binding [idx/*recursive-traversal-stats* stats] + page (binding [engine/*recursive-traversal-stats* stats] (eacl/lookup-resources acl (assoc query :first 3 :after after)))] (is (<= (:advanced-datoms @stats 0) ceiling) diff --git a/modules/eacl-datomic/test/eacl/datomic/cache_review_regressions_test.clj b/modules/eacl-datomic/test/eacl/datomic/cache_review_regressions_test.clj index c7ee2555f..e27a8cab4 100644 --- a/modules/eacl-datomic/test/eacl/datomic/cache_review_regressions_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/cache_review_regressions_test.clj @@ -3,7 +3,9 @@ See docs/reports/2026-07-31-eacl-v8.0-cache-adversarial-review.md. The critical pagination finding (C1) is covered by - eacl.datomic.cache-differential-test." + eacl.datomic.cache-differential-test, and M1 (identical reads at one basis + compute once) by eacl.datomic.consistency-cache-test/ + can-results-obey-all-cache-consistency-modes-test." (:require [clojure.set] [clojure.string :as str] [clojure.test :refer [deftest is testing]] @@ -89,9 +91,7 @@ :after (get-in page-1 [:page-info :end-cursor])))] - (is (= ["a3"] (mapv :id (:data page-2)))) - (is (nil? (get-in page-2 - [:page-info :cursor-recovery])))))))) + (is (= ["a3"] (mapv :id (:data page-2))))))))) (deftest explicit-cache-true-does-not-fragment-answer-keys-test ;; :cache? selects how to obtain an answer, not which answer was requested. @@ -358,8 +358,7 @@ (is (= :lookup-resources (:operation data))) (is (false? (:historical? data))) (is (= (set gone) (set (:entity-ids data))) - "every offending eid is reported, so one repair pass fixes them all") - (is (str/includes? (:cause data "") ""))) + "every offending eid is reported, so one repair pass fixes them all")) (testing "the message names the cause and the repair tool" (let [message (try (eacl/lookup-resources acl {:subject (spice-object :user "alice") @@ -372,31 +371,6 @@ (is (not (str/includes? message "cache")) "this fires with {:cache shared-cache/no-cache} too; it must not be diagnosed as a cache fault"))))))) -;; --- M1 --------------------------------------------------------------------- - -(deftest fully-consistent-reads-reuse-the-basis-pinned-exact-entry-test - ;; The exact key pins the complete source lineage, schema generation, - ;; operation, query identity, and basis revision. One source at one revision - ;; therefore maps to exactly one immutable database value. - (with-mem-conn [conn schema/v8-schema] - (let [acl (core/make-client conn {:security-key token-key - :cache {}}) - _ (seed-direct! conn acl 1) - alice (spice-object :user "alice") - account (spice-object :account "acct0") - calls (atom 0) - original engine/check-evidence-eids] - (with-redefs [engine/check-evidence-eids (fn [& args] - (swap! calls inc) - (apply original args))] - (dotimes [_ 3] (is (true? (eacl/can? acl alice :admin account)))) - (is (= 1 @calls) "identical fully-consistent reads at one basis compute once") - - (testing "a relationship change still invalidates, because basis-t moves" - (eacl/delete-relationship! acl (->Relationship alice :owner account)) - (is (false? (eacl/can? acl alice :admin account))) - (is (= 2 @calls))))))) - ;; --- M2 --------------------------------------------------------------------- (defn- forged-token @@ -522,8 +496,6 @@ (is (= ["acct3" "acct4" "acct5"] (mapv :id (:data recovered-1)))) (is (= (:data recovered-1) (:data recovered-2))) - (is (nil? (get-in recovered-1 - [:page-info :cursor-recovery]))) (is (false? (:cached? recovered-1)) "first historical recovery has its own complete exact key") (is (true? (:cached? recovered-2))) diff --git a/modules/eacl-datomic/test/eacl/datomic/consistency_v3_test.clj b/modules/eacl-datomic/test/eacl/datomic/consistency_v3_test.clj index 79deddc05..d4b81c6b3 100644 --- a/modules/eacl-datomic/test/eacl/datomic/consistency_v3_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/consistency_v3_test.clj @@ -355,8 +355,7 @@ (eacl/lookup-resources authorization (assoc query :after cursor))] - (is (= ["doc-b"] (mapv :id (:data page-2)))) - (is (nil? (get-in page-2 [:page-info :cursor-recovery]))))) + (is (= ["doc-b"] (mapv :id (:data page-2)))))) (let [fresh-page-1 (eacl/lookup-resources authorization query) fresh-cursor @@ -372,8 +371,7 @@ (eacl/lookup-resources authorization (assoc query :after fresh-cursor))] - (is (= ["doc-b"] (mapv :id (:data page)))) - (is (nil? (get-in page [:page-info :cursor-recovery]))))) + (is (= ["doc-b"] (mapv :id (:data page)))))) (testing "a changed causal floor is a different query scope" (is (= :eacl.pagination/invalid-cursor (:type diff --git a/modules/eacl-datomic/test/eacl/datomic/impl/indexed_test.clj b/modules/eacl-datomic/test/eacl/datomic/impl/indexed_test.clj index 7c38c42d5..711d2a023 100644 --- a/modules/eacl-datomic/test/eacl/datomic/impl/indexed_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/impl/indexed_test.clj @@ -1069,39 +1069,20 @@ (deftest recursive-arrow-permission-lookup-resources-visited-state-test (with-mem-conn [conn schema/v8-schema] - (let [db (load-recursive-parent-db! conn) - user (recursive-user-ref "user-1") - reader-relation-eid (:db/id (impl.indexed/find-relation-def db :account :reader)) - parent-relation-eid (:db/id (impl.indexed/find-relation-def db :account :parent)) - reader-path {:type :relation - :name :reader - :subject-type :user - :relation-eid reader-relation-eid} - recursive-paths [reader-path - {:type :arrow - :via :parent - :target-type :account - :via-relation-eid parent-relation-eid - :target-permission :read - :sub-paths [reader-path]}]] + (let [db (load-recursive-parent-db! conn) + user (recursive-user-ref "user-1")] (testing "lookup-resources should not stop recursion only because the permission name repeats on a different resource" - (with-redefs [impl.indexed/get-permission-paths - (fn [_db resource-type permission-name] - (if (and (= :account resource-type) - (= :read permission-name)) - recursive-paths - []))] - (is (= #{(spice-object :account "root") - (spice-object :account "child") - (spice-object :account "grandchild")} - (paginated->spice-set db - (lookup-resources db {:subject user - :permission :read - :resource/type :account - :first 100})))) - (is (= 3 (:count (count-resources db {:subject user - :permission :read - :resource/type :account}))))))))) + (is (= #{(spice-object :account "root") + (spice-object :account "child") + (spice-object :account "grandchild")} + (paginated->spice-set db + (lookup-resources db {:subject user + :permission :read + :resource/type :account + :first 100})))) + (is (= 3 (:count (count-resources db {:subject user + :permission :read + :resource/type :account})))))))) (deftest recursive-dependency-closure-traversal-tests (with-mem-conn [conn schema/v8-schema] @@ -1141,13 +1122,19 @@ (is (= (first eids) (get-in page [:page-info :start-cursor :result-eid]))))) - (testing "recursive lookup does not call public can? while paging" - (with-redefs [impl.indexed/can? (fn [& _] - (throw (ex-info "can? should not be called by pagination" {})))] - (is (= 2 (count (:data (lookup-resources db {:subject user - :permission :read - :resource/type :account - :first 2}))))))) + (testing "recursive lookup does not run point checks while paging" + (let [point-check (fn [& _] + (throw (ex-info "a point check should not be run by pagination" {})))] + (with-redefs [engine/can-eids? point-check + engine/check-evidence-eids point-check] + (is (thrown-with-msg? clojure.lang.ExceptionInfo + #"point check should not be run" + (can? db user :read (recursive-account-ref "root"))) + "the public check goes through the redefined entry points") + (is (= 2 (count (:data (lookup-resources db {:subject user + :permission :read + :resource/type :account + :first 2})))))))) (testing "bare recursive :last requires explicit complete evaluation" (binding [engine/*evaluation-mode* :complete-denotation] @@ -1256,13 +1243,6 @@ :permission :view :resource/type :server})))))))) -(deftest indexed-facade-has-no-shared-schema-cache-surface-test - (is (nil? (ns-resolve 'eacl.datomic.impl.indexed '*schema-cache*))) - (is (nil? (ns-resolve 'eacl.datomic.impl.indexed 'make-schema-cache))) - (is (nil? (ns-resolve 'eacl.datomic.impl.indexed - 'evict-permission-paths-cache!))) - (is (nil? (ns-resolve 'eacl.engine.v8 'make-schema-cache)))) - (deftest string-object-id-resolution-test ;; d/entid on a bare string throws a raw IllegalArgumentException, which ;; leaked out of impl-level reads. Strings now resolve via the canonical diff --git a/modules/eacl-datomic/test/eacl/datomic/lookup_cache_test.clj b/modules/eacl-datomic/test/eacl/datomic/lookup_cache_test.clj index 49d5c0689..b7a874ffa 100644 --- a/modules/eacl-datomic/test/eacl/datomic/lookup_cache_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/lookup_cache_test.clj @@ -8,7 +8,6 @@ [eacl.datomic.datomic-helpers :refer [with-mem-conn with-mem-conns]] [eacl.datomic.impl :as impl] - [eacl.datomic.impl.indexed :as idx] [eacl.datomic.schema :as schema] [eacl.engine.v8 :as engine])) @@ -371,15 +370,18 @@ cursor (get-in first-page [:page-info :end-cursor]) expected-page (eacl/lookup-resources first-client (assoc query :after cursor)) - stats (atom {})] - (is (= (:data expected-page) - (:data - (binding [idx/*recursive-traversal-stats* stats] - (eacl/lookup-resources second-client - (assoc query :after cursor))))) + stats (atom {}) + replayed (binding [engine/*recursive-traversal-stats* stats] + (eacl/lookup-resources second-client + (assoc query :after cursor)))] + (is (= (:data expected-page) (:data replayed)) "another client replays the cursor against its authenticated snapshot") - (is (nil? (:recursive-page-hits @stats)) - "no unauthenticated recursive page is reused across clients"))))) + (is (false? (:cached? replayed)) + "no page the first client rendered is reused across clients") + (is (zero? (get @stats :continuation-hits 0)) + "no checkpoint the first client retained is reused across clients") + (is (pos? (get @stats :derived-grants 0)) + "the second client derives the page from its own snapshot"))))) (deftest recursive-cursors-resume-from-the-client-private-denotation-test (with-mem-conn [conn schema/v8-schema] @@ -409,7 +411,7 @@ (let [first-page (eacl/lookup-resources client query) stats (atom {}) second-page - (binding [idx/*recursive-traversal-stats* stats] + (binding [engine/*recursive-traversal-stats* stats] (eacl/lookup-resources client (assoc query @@ -421,7 +423,9 @@ ;; the closure. The stable engine resumes from the client-private ;; checkpoint and derives only the next page plus lookahead, so the ;; bound is page-proportional rather than zero. - (is (<= (get @stats :derived-grants 0) 4) + (is (= 1 (get @stats :continuation-hits 0)) + "a later page resumes the client-private checkpoint") + (is (<= 1 (get @stats :derived-grants 0) 4) "a later page resumes private state with page-bounded work")) (testing "a bounded shared cache does not disturb denotation reuse" (let [bounded-client @@ -432,17 +436,19 @@ first-page (eacl/lookup-resources bounded-client query) stats (atom {}) second-page - (binding [idx/*recursive-traversal-stats* stats] + (binding [engine/*recursive-traversal-stats* stats] (eacl/lookup-resources bounded-client (assoc query :after (get-in first-page [:page-info :end-cursor]))))] (is (= ["child"] (mapv :id (:data second-page)))) - ;; The tiny weight budget may evict the checkpoint; governed - ;; replay of a three-folder chain stays below the closure bound. - (is (<= (get @stats :derived-grants 0) 10) - "an evicted checkpoint replays a bounded prefix, never the closure")))))) + ;; The continuation store holds as many checkpoints as the cache + ;; holds entries, so the one the first page left is still there. + (is (= 1 (get @stats :continuation-hits 0)) + "the one retained checkpoint serves the next page") + (is (<= 1 (get @stats :derived-grants 0) 4) + "the next page is derived with page-bounded work, never the closure")))))) (deftest long-count-does-not-hold-relationship-writer-test (with-mem-conn [conn schema/v8-schema] @@ -780,15 +786,3 @@ :security-key "provenance0000000000000000000000"})] (is (false? (:cached? (eacl/lookup-resources plain query)))) (is (false? (:cached? (eacl/count-resources plain query))))))))) - -(deftest default-client-cache-has-no-ttl-test - (with-mem-conn [conn schema/v8-schema] - (is (nil? (:lookup-cache-ttl-ms - (:runtime (core/make-client conn {})))) - "client-private authorization results do not expire by wall clock") - (let [error (try - (core/make-client conn {:cache {:ttl-ms 5000}}) - nil - (catch clojure.lang.ExceptionInfo ex ex))] - (is (= :eacl/invalid-config (:type (ex-data error)))) - (is (= [:ttl-ms] (:unknown-keys (ex-data error))))))) diff --git a/modules/eacl-datomic/test/eacl/datomic/raw_op_count_test.clj b/modules/eacl-datomic/test/eacl/datomic/raw_op_count_test.clj index ec55a1133..bf75d082f 100644 --- a/modules/eacl-datomic/test/eacl/datomic/raw_op_count_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/raw_op_count_test.clj @@ -3,9 +3,10 @@ The raw impl API is the 0tx consumer surface: bare immutable db values, no client caches. Envelopes are the ratcheted numbers recorded in - formal/baselines/recursive-op-count-envelopes.edn (V1/V2 current - truth: two schema proofs and two plan compiles per raw list request; - zero proofs per raw point check). Per-push, no wall-clock assertions." + formal/baselines/recursive-op-count-envelopes.edn. Every measurement is + taken from an observer that production writes on this path; the + self-checks below fail when one of them goes quiet. Per-push, no + wall-clock assertions." (:require [clojure.edn :as edn] [clojure.test :refer [deftest is testing use-fixtures]] [datomic.api :as d] @@ -17,6 +18,9 @@ [eacl.datomic.impl.indexed :as impl.indexed] [eacl.datomic.schema :as dschema] [eacl.engine.v8 :as engine] + [eacl.formal.production-kernel :as production] + [eacl.request.counters :as request-counters] + [eacl.subproblem-cache :as subproblem] [eacl.test-support.repo :as repo] [eacl.verified-kernel :as verified])) @@ -63,28 +67,39 @@ (d/delete-database (:uri @state)))))) (defn- measured - "The raw Datomic facade rebinds engine/*recursive-traversal-stats* to + "Runs one raw request with every observer bound. + + The raw Datomic facade rebinds engine/*recursive-traversal-stats* to impl.indexed's dynamic (with-shared-engine), so raw callers observe - through the impl-level var." + through the impl-level var. :scans is :advanced-datoms, the adapter + commands the stable engine issued; :crossings sums every generated-kernel + invocation; :plan-seals is the request ledger's :seals. Denotation key + builds have no counter of their own, so they are counted by binding a + counting key constructor." [f] - (let [kx (atom {}) bops (atom {}) rts (atom {}) shape (atom {})] - (binding [verified/*kernel-crossing-stats* kx - backend/*backend-op-stats* bops - impl.indexed/*recursive-traversal-stats* rts - engine/*request-shape-stats* shape] + (let [crossings (atom {}) backend-ops (atom {}) traversal (atom {}) + shape (atom {}) key-builds (atom 0) + ledger (request-counters/make-ledger)] + (binding [verified/*kernel-crossing-stats* crossings + backend/*backend-op-stats* backend-ops + impl.indexed/*recursive-traversal-stats* traversal + engine/*request-shape-stats* shape + request-counters/*ledger* ledger + subproblem/*exact-denotation-key-fn* + (fn [_] + (swap! key-builds inc) + nil)] (f)) - {:proof-frame (get @bops :proof-frame 0) - :plan-compiles (get @rts :compiled-recursive-plans 0) - :key-builds (get @shape :denotation-key-builds 0) - :dep-calcs (get @shape :denotation-dependency-calcs 0) - :drive (get @kx :indexed-traversal-drive 0) - :resume (get @kx :indexed-traversal-resume 0) - :stream-fills (get @rts :stream-fills 0) - :advanced (get @rts :advanced-datoms 0) - :derived-grants (get @rts :derived-grants 0)})) + {:proof-frame (get @backend-ops :proof-frame 0) + :plan-seals (:seals (request-counters/snapshot ledger)) + :key-builds @key-builds + :path-calcs (get @shape :permission-path-calcs 0) + :crossings (reduce + (vals @crossings)) + :scans (get @traversal :advanced-datoms 0) + :derived-grants (get @traversal :derived-grants 0)})) (defn- assert-crossing-law! - [render-kind {:keys [drive resume stream-fills advanced]}] + [render-kind {:keys [crossings scans]}] (let [{default-batch-size :batch-size page-batch-size :page-batch-size :keys [constant fuel]} @@ -92,16 +107,12 @@ batch-size (if (= :page render-kind) page-batch-size default-batch-size) - batches (quot (+ stream-fills (dec batch-size)) batch-size) - fuel-yields (quot advanced fuel)] - (is (<= resume stream-fills) - "one ordered response wave resumes one or more backend scans") - (is (<= drive (+ resume 1 fuel-yields)) - ":indexed-traversal-drive bounded by response waves + completion + fuel yields") - (is (<= (+ drive resume) + batches (quot (+ scans (dec batch-size)) batch-size) + fuel-yields (quot scans fuel)] + (is (<= crossings (+ (* 2 batches) constant fuel-yields)) (str (name render-kind) - " crossings <= 2*ceil(streams/batch)+recorded constant")))) + " crossings <= 2*ceil(scans/batch)+recorded constant")))) (deftest raw-lookup-op-count-test (let [e (:raw-lookup-first-50 envelopes) @@ -111,20 +122,22 @@ db {:subject {:type :user :id user-1-eid} :permission :view :resource/type :account :first 50}))] - (testing "recursion active (suite self-check)" - ;; :stream-fills belonged to the retired streaming engine; the stable - ;; engine's physical work shows up as :advanced-datoms (commands). - (is (pos? (:advanced m)) (pr-str m)) - (is (pos? (:derived-grants m)) (pr-str m))) + (testing "recursion active and every observer live (suite self-check)" + (is (pos? (:scans m)) (pr-str m)) + (is (pos? (:derived-grants m)) (pr-str m)) + (is (pos? (:plan-seals m)) (pr-str m)) + (is (pos? (:path-calcs m)) (pr-str m)) + (is (pos? (:crossings m)) (pr-str m))) (testing "ordered-generation frames per raw list request" (is (<= (:proof-frame m) (:maximum-proof-frame-reads e)) (pr-str m))) - (testing "recursive plan compiles per raw request (:compiled-recursive-plans)" - (is (<= (:plan-compiles m) (:maximum-plan-compiles e)) (pr-str m))) + (testing "plan seals per raw request (ledger :seals)" + (is (<= (:plan-seals m) (:maximum-plan-compiles e)) (pr-str m))) (testing "denotation cache-key work against a nil store" - (is (<= (:key-builds m) (:maximum-denotation-key-builds e)) (pr-str m)) - (is (<= (:dep-calcs m) (:maximum-denotation-dependency-calcs e)) (pr-str m))) - (testing "streaming early-stop scan envelope (:stream-fills)" - (is (<= (:stream-fills m) (:maximum-backend-scans e)) (pr-str m))) + (is (<= (:key-builds m) (:maximum-denotation-key-builds e)) (pr-str m))) + (testing "permission path calculations (:permission-path-calcs)" + (is (<= (:path-calcs m) (:maximum-permission-path-calcs e)) (pr-str m))) + (testing "early-stop scan envelope (:advanced-datoms)" + (is (<= (:scans m) (:maximum-backend-scans e)) (pr-str m))) (assert-crossing-law! :page m))) (deftest raw-can-op-count-test @@ -140,13 +153,23 @@ (testing (str label " raw point check") (is (<= (:proof-frame m) (:maximum-proof-frame-reads e)) (str label " :proof-frame " (pr-str m))) - (is (<= (:plan-compiles m) (:maximum-plan-compiles e)) - (str label " :compiled-recursive-plans " (pr-str m))) + (is (pos? (:scans m)) + (str label " point check reads the backend " (pr-str m))) + (is (<= (:plan-seals m) (:maximum-plan-compiles e)) + (str label " plan seals " (pr-str m))) (is (zero? (:key-builds m)) (str label " raw can? builds no denotation keys " (pr-str m))) - (is (<= (:stream-fills m) (:maximum-backend-scans e)) + (is (<= (:scans m) (:maximum-backend-scans e)) (str label " bounded reverse point check " (pr-str m))) - (assert-crossing-law! :order-independent m))))) + (assert-crossing-law! :order-independent m))) + (testing "the key-build counter is live: the same check keys its reuse lookups once a store is bound" + (is (pos? (:key-builds + (binding [subproblem/*store* + (subproblem/store {:denotation-max-entries 16 + :answer-max-entries 2})] + (measured + #(dimpl/can? db {:type :user :id user-1-eid} :view + {:type :account :id deep-child-eid}))))))))) (deftest raw-count-linearity-test (let [e (:count-full envelopes) @@ -163,23 +186,46 @@ (is (<= (:derived-grants m) (* (:maximum-derived-grants-factor e) (inc accounts))) (pr-str m))) - (testing "scan count linear in fixture size (:stream-fills)" - (is (<= (:stream-fills m) + (testing "scan count linear in fixture size (:advanced-datoms)" + (is (pos? (:scans m)) (pr-str m)) + (is (<= (:scans m) (+ accounts (:maximum-backend-scans-slack e))) (pr-str m))) (assert-crossing-law! :order-independent m))) (deftest interned-empty-response-immutability-test ;; 4.2 pin: the interned empty scan-response payload must stay empty - ;; after traversal storms — generated code mutates only freshly - ;; constructed wrappers (the collection shims' contract). The suite's - ;; other tests have already driven thousands of empty responses - ;; through the interned instance by the time this runs. - (let [{:keys [db user-1-eid]} @state] - (dimpl/count-resources - db {:subject {:type :user :id user-1-eid} - :permission :view :resource/type :account}) - (is (zero? (.cardinalityInt - ^dafny.DafnySequence - @@(resolve 'eacl.formal.production-kernel/empty-values-sequence))) + ;; after the generated validator has been handed it many times — + ;; generated code mutates only freshly constructed wrappers (the + ;; collection shims' contract). A fresh interned instance shows that + ;; these responses, and nothing earlier in the JVM, are what realized it. + (let [interned (delay (#'production/dafny-sequence [])) + exchange {:command {:request-scope 31 + :request-id 7 + :projection {:kind :subject->resources + :subject-type "user" + :subject-eid 1 + :relation-eid 2 + :resource-type "document" + :bound-eid 10} + :chunk-size 3} + :response {:request-scope 31 + :request-id 7 + :values [] + :terminal? true + :fetched-values 0}}] + (with-redefs [production/empty-values-sequence interned] + (is (every? #(= {:status :accepted + :values [] + :terminal? true + :fetched-values 0} + %) + (repeatedly + 1000 + #(verified/decide production/default-selection + :indexed-scan-response + exchange))))) + (is (realized? interned) + "an empty scan response is handed to the validator as the interned payload") + (is (zero? (.cardinalityInt ^dafny.DafnySequence @interned)) "interned empty DafnySequence mutated by generated code"))) diff --git a/modules/eacl-datomic/test/eacl/datomic/recursive_cache_test.clj b/modules/eacl-datomic/test/eacl/datomic/recursive_cache_test.clj index 1e9e0c310..91dad323b 100644 --- a/modules/eacl-datomic/test/eacl/datomic/recursive_cache_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/recursive_cache_test.clj @@ -427,7 +427,7 @@ "an alternate cache resolves its own denotation instead of trusting foreign state") (is (true? (:cached? retry-page2)) "a retry reuses the originating client's completed answer") - (is (zero? (stat retry-stats :stream-fills)) + (is (= {} @retry-stats) "an answer hit does not re-enter recursive traversal") (is (<= (stat previous-stats :derived-grants) 30) "bounded prefix replay retains at most the requested window"))))) @@ -497,8 +497,7 @@ (eacl/lookup-resources replay-client (assoc query :after cursor))]]] (is (= expected (:data recovered)) - "Datomic resumes the immutable cursor snapshot without a hybrid walk") - (is (nil? (get-in recovered [:page-info :cursor-recovery])))) + "Datomic resumes the immutable cursor snapshot without a hybrid walk")) (is (= "new-live-account" (-> (collect-forward cached-client query) :data peek :id)) "a new enumeration observes the relationship write"))))) @@ -589,8 +588,6 @@ (range 5 10)) (:data page2)) "the continuation resumes exclusively after the boundary") - (is (nil? (get-in page2 [:page-info :cursor-recovery])) - "unrelated churn is a continuation hit, not a recovery") (is (pos? (get @crossings :cursor-continuation 0)) "the reuse is a verified kernel decision, not a bypass") ;; Governed replay to the boundary plus one fresh page on the @@ -699,15 +696,13 @@ (is (= (mapv account-id (range 5 10)) (mapv :id (:data recovered))) "the cursor resumes against the retained immutable snapshot") - (is (not= (:data fresh-page1) (:data recovered))) - (is (nil? (get-in recovered [:page-info :cursor-recovery]))))) + (is (not= (:data fresh-page1) (:data recovered))))) (testing "a later live subject deletion still cannot rewrite history" (eacl/delete-object! client subject) @(d/transact conn [[:db.fn/retractEntity subject-eid]]) (let [recovered (eacl/lookup-resources client (assoc query :after cursor))] (is (= (mapv account-id (range 5 10)) - (mapv :id (:data recovered)))) - (is (nil? (get-in recovered [:page-info :cursor-recovery]))))))))) + (mapv :id (:data recovered)))))))))) (deftest alternate-cache-resolves-its-own-denotation-for-a-foreign-cursor-test (with-mem-conn [conn schema/v8-schema] diff --git a/modules/eacl-datomic/test/eacl/datomic/schema_basis_test.clj b/modules/eacl-datomic/test/eacl/datomic/schema_basis_test.clj index 0a72f45d9..8c96cbc0d 100644 --- a/modules/eacl-datomic/test/eacl/datomic/schema_basis_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/schema_basis_test.clj @@ -136,9 +136,7 @@ (eacl/write-schema! acl schema-viewer-only) (let [page2 (eacl/lookup-resources acl (assoc query :after cursor))] (is (= 1 (count (:data page2)))) - (is (not= (:data page1) (:data page2))) - (is (nil? (get-in page2 [:page-info :cursor-recovery])) - "exact continuation has no rebase/restart marker")) + (is (not= (:data page1) (:data page2)))) (is (empty? (:data (eacl/lookup-resources acl query))) "a new enumeration uses the new schema generation")))) diff --git a/modules/eacl-datomic/test/eacl/datomic/schema_test.clj b/modules/eacl-datomic/test/eacl/datomic/schema_test.clj index 439fea042..a334ae007 100644 --- a/modules/eacl-datomic/test/eacl/datomic/schema_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/schema_test.clj @@ -239,34 +239,11 @@ (:reason (exception-data #(schema/read-schema (d/db conn))))))))) -(deftest schema-does-not-include-persisted-grants-test - (testing "recursive traversal does not require persisted effective grant attrs" - (let [idents (set (map :db/ident schema/v8-schema))] - (is (not (contains? idents :eacl.v7.grant/subject-type+permission+resource-type+resource))) - (is (not (contains? idents :eacl.v7.grant/resource-type+permission+subject-type+subject))) - (is (not (contains? idents :eacl.grant/indexed-node)))))) - -(deftest schema-does-not-include-derived-expression-metrics-test - (let [idents (set (map :db/ident schema/v8-schema))] - (is (empty? - (clojure.set/intersection - idents - expression-persistence/retired-expression-attributes))))) - (deftest clean-v8-schema-retires-flat-permission-attributes-test - (let [idents (set (map :db/ident schema/v8-schema))] - (is (empty? - (clojure.set/intersection - idents - expression-persistence/legacy-flat-attributes))) - (is (empty? - (clojure.set/intersection - idents - expression-persistence/retired-expression-attributes))) - (with-mem-conn [conn schema/v8-schema] - (schema/write-schema! conn direct-storage-schema) - (is (= :expression - (schema/permission-storage-shape (d/db conn))))))) + (with-mem-conn [conn schema/v8-schema] + (schema/write-schema! conn direct-storage-schema) + (is (= :expression + (schema/permission-storage-shape (d/db conn)))))) (deftest eacl-schema-comparison-tests (testing "we can calculate additions & retractions" diff --git a/modules/eacl-datomic/test/eacl/datomic/speculative_admission_test.clj b/modules/eacl-datomic/test/eacl/datomic/speculative_admission_test.clj index 651b34c80..4f3b3ebfe 100644 --- a/modules/eacl-datomic/test/eacl/datomic/speculative_admission_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/speculative_admission_test.clj @@ -65,7 +65,6 @@ (eacl/->Relationship alice :viewer report)])) (deftest caller-native-database-values-have-no-public-constructor-test - (is (nil? (ns-resolve 'eacl.datomic.core 'snapshot))) (with-mem-conn [conn datomic-schema/v8-schema] (let [db (d/db conn) values @@ -444,5 +443,10 @@ prospective {:resource doc :permission :view}))) (let [after (datomic/cache-stats client)] (is (= (:puts before) (:puts after))) - (is (= (:exact-size before) (:exact-size after))) - (is (= (:managed-size before) (:managed-size after))))))))))) + (is (= (:exact-entries before) (:exact-entries after))) + (is (= (:managed-entries before) (:managed-entries after))) + (eacl/check-permission base demand) + (let [committed (datomic/cache-stats client)] + (is (< (:puts after) (:puts committed)) + "the same check against the committed snapshot publishes") + (is (< (:exact-entries after) (:exact-entries committed)))))))))))) diff --git a/modules/eacl-datomic/test/eacl/datomic/trusted_surface_audit_test.clj b/modules/eacl-datomic/test/eacl/datomic/trusted_surface_audit_test.clj deleted file mode 100644 index 1d8576286..000000000 --- a/modules/eacl-datomic/test/eacl/datomic/trusted_surface_audit_test.clj +++ /dev/null @@ -1,72 +0,0 @@ -(ns eacl.datomic.trusted-surface-audit-test - "Pins the trusted-surface-hygiene deletions (11.1): the enumerated dead - paths must not return, and the live survivors they were entangled with - must still exist. Var probes use requiring-resolve so a reintroduced - definition fails this suite even if nothing else calls it." - (:require [clojure.java.io :as io] - [clojure.test :refer [deftest is testing]] - [eacl.datomic.core :as core] - [eacl.datomic.datomic-helpers :refer [with-mem-conn]] - [eacl.datomic.schema :as schema])) - -(defn- var-absent? - [sym] - (nil? (try - (requiring-resolve sym) - (catch java.io.FileNotFoundException _ nil)))) - -(defn- var-present? - [sym] - (some? (requiring-resolve sym))) - -(deftest deleted-trusted-surfaces-stay-deleted-test - (testing "the watermark namespace is gone" - (is (nil? (io/resource "eacl/datomic/watermark.clj")))) - (testing "the Datomic provider-cache path is gone; the core sentinel survives" - (is (nil? (io/resource "eacl/datomic/cache.clj"))) - (is (nil? (io/resource "eacl/datomic/cache_store_contract.clj"))) - (is (var-absent? 'eacl.cache/resolve!)) - (is (var-absent? 'eacl.cache/local-store)) - (is (var-absent? 'eacl.cache/cache-store)) - (is (var-absent? 'eacl.datomic.cache/authenticated-store)) - (is (var-absent? 'eacl.datomic.cache/CacheStore)) - (is (var-absent? 'eacl.datomic.cache/LocalStore)) - (is (var-absent? 'eacl.datomic.cache/local-store)) - (is (var-present? 'eacl.cache/no-cache)) - (is (var-present? 'eacl.cache/resolve-basis!))) - (testing "dead observed-revision checkpoints are gone; key derivation survives" - (is (var-absent? 'eacl.datomic.consistency/zed-token)) - (is (var-absent? 'eacl.datomic.consistency/token-data)) - (is (var-absent? 'eacl.datomic.consistency/token-revision)) - (is (var-absent? 'eacl.datomic.consistency/derive-signing-key)) - (is (var-absent? 'eacl.datomic.consistency/revision-checkpoints)) - (is (var-absent? 'eacl.datomic.consistency/observe!)) - (is (var-absent? - 'eacl.datomic.consistency/revision-at-least-seconds-ago))) - (testing "cursor edges carry no path frontiers" - (let [relay-source (slurp (io/resource "eacl/relay.cljc"))] - (is (not (re-find #":path-frontiers" relay-source)) - "the relay edge coercion must not resurrect frontier transport"))) - (testing "changed-proof cursor rebase and restart machinery is gone" - (doseq [resource ["eacl/relay.cljc" - "eacl/engine/v8.cljc" - "eacl/datomic/core.clj"] - :let [source (slurp (io/resource resource))]] - (is (not (re-find #":rebase\?|:cursor-recovery|mark-recursive-restart|restart-unroutable-rebase|keyset-rebase|rebase-acyclic-query" - source)) - (str resource " must fail closed instead of rebasing or restarting cursors")))) - (testing "EACL authorization owns no blocking coordinator" - (doseq [resource ["eacl/datomic/core.clj" - "eacl/cache.cljc" - "eacl/subproblem_cache.cljc"] - :let [source (slurp (io/resource resource))]] - (is (not (re-find #"\(locking\b|schema-lock|ReentrantReadWriteLock|Semaphore|single[- ]flight" - source)) - (str resource " must stay free of EACL-owned blocking coordination")))) - (testing "the Datomic-only answer-kind registry is gone" - (is (var-absent? 'eacl.datomic.core/answer-cache-kinds))) - (testing "the write-only provider options are gone from client opts" - (with-mem-conn [conn schema/v8-schema] - (let [client (core/make-client conn {:security-key "audit-test0000000000000000000000"})] - (is (not (contains? (:runtime client) :shared-cache-store))) - (is (not (contains? (:runtime client) :lookup-cache-store))))))) diff --git a/modules/eacl-datomic/test/eacl/datomic/v8_characterization_test.clj b/modules/eacl-datomic/test/eacl/datomic/v8_characterization_test.clj index c6ed8f1ae..ada6ac75a 100644 --- a/modules/eacl-datomic/test/eacl/datomic/v8_characterization_test.clj +++ b/modules/eacl-datomic/test/eacl/datomic/v8_characterization_test.clj @@ -6,7 +6,6 @@ [datomic.api :as d] [eacl.cache :as shared-cache] [eacl.core :as eacl] - [eacl.contract-support :as contract] [eacl.datomic.core :as core] [eacl.datomic.datomic-helpers :refer [with-mem-conn]] [eacl.datomic.schema :as schema] @@ -157,15 +156,3 @@ :read (folder "folder-3")))) (is (= 3 (:count (eacl/count-resources client query)))))))) - -(deftest public-api-arity-characterization-test - (with-mem-conn [conn schema/v8-schema] - (let [client (core/make-client - conn - {:security-key "v8-public-api-arity-characterization"})] - (eacl/write-schema! client contract/smoke-schema) - @(d/transact conn - (mapv (fn [{:keys [id]}] {:eacl/id id}) - contract/smoke-objects)) - (eacl/create-relationships! client contract/smoke-relationships) - (contract/assert-public-api-arity-contract! client)))) diff --git a/modules/eacl-datomic/test/eacl/migrations/v6_to_v7_test.clj b/modules/eacl-datomic/test/eacl/migrations/v6_to_v7_test.clj index 9d8eb3c34..f0138fc61 100644 --- a/modules/eacl-datomic/test/eacl/migrations/v6_to_v7_test.clj +++ b/modules/eacl-datomic/test/eacl/migrations/v6_to_v7_test.clj @@ -259,13 +259,6 @@ (is (thrown? clojure.lang.ExceptionInfo (eacl.datomic/make-client conn {})) "Empty legacy schemas also require explicit upgrade/bootstrap."))) -(deftest migrate!-rejects-unknown-options-test - (with-mem-conn [conn v6-schema] - (let [ex (try (mig/migrate! conn {:shcema schema-str}) nil - (catch clojure.lang.ExceptionInfo e e))] - (is (some? ex)) - (is (= :eacl/invalid-config (:type (ex-data ex))))))) - (deftest future-storage-version-refused-test ;; A stamp from a future storage model means this build predates the data's ;; migration; running anyway would silently answer false/empty. diff --git a/modules/eacl-datomic/test/eacl/spice_test.clj b/modules/eacl-datomic/test/eacl/spice_test.clj index 7bd1f0f97..a7940fd89 100644 --- a/modules/eacl-datomic/test/eacl/spice_test.clj +++ b/modules/eacl-datomic/test/eacl/spice_test.clj @@ -520,9 +520,7 @@ :after page1-end-cursor))] (is (= (:data expected-page2) (:data recovered))) - (is (not-any? #(= new-server %) (:data recovered))) - (is (nil? (get-in recovered - [:page-info :cursor-recovery]))))) + (is (not-any? #(= new-server %) (:data recovered))))) (let [base-query {:resource/type :server :permission :view :subject (->user "super-user")} @@ -548,9 +546,7 @@ (assoc base-query :first 2 :after page1-end-cursor))] - (is (some #(= victim %) (:data recovered))) - (is (nil? (get-in recovered - [:page-info :cursor-recovery])))))) + (is (some #(= victim %) (:data recovered)))))) (testing "spice-read-relationships results are constrained by filters for resource type & ID" (testing "transact the test entities we are about to use" diff --git a/modules/eacl/test/eacl/authorization/inspection_test.cljc b/modules/eacl/test/eacl/authorization/inspection_test.cljc index 39e9c816e..1a14bb1ba 100644 --- a/modules/eacl/test/eacl/authorization/inspection_test.cljc +++ b/modules/eacl/test/eacl/authorization/inspection_test.cljc @@ -6,10 +6,12 @@ [eacl.relationships.inspection :as inspection])) (deftest stored-inspection-never-evaluates-or-compiles-a-caveat - (doseq [time [99 100 101]] + (doseq [time [99 100 101] + ;; Inspection needs no evaluator and never calls one it is given. + evaluator [{:evaluator nil} {}]] (let [calls (atom 0) reads (atom {}) - request (fixtures/request {:time time :calls calls :reads reads :evaluator nil})] + request (fixtures/request (merge {:time time :calls calls :reads reads} evaluator))] (with-redefs [plan/compile-plan (fn [& _] (throw (ex-info "Unexpected compilation" {})))] (is (= {:caveat "enabled" :valid-until-ms 100} (qualification/inspect request 1 3))) diff --git a/modules/eacl/test/eacl/backend/v8_test.cljc b/modules/eacl/test/eacl/backend/v8_test.cljc index d67d1693a..5dcf1778d 100644 --- a/modules/eacl/test/eacl/backend/v8_test.cljc +++ b/modules/eacl/test/eacl/backend/v8_test.cljc @@ -1034,19 +1034,6 @@ adapter :user 1 10 :document 3))) (is (= (+ 2 before) (:direct-match-probes @work)))))))) -(deftest projection-cache-free-path-has-no-cache-effects-test - (let [adapter (projection-test-adapter) - work (atom {})] - (binding [subproblem/*store* nil - engine/*backend-work-stats* work] - (dotimes [_ 2] - (is (= (vec (range 1 6)) - (vec - (take 5 - (engine/subject->resources - adapter :user 1 10 :document nil)))))) - (is (= 2 (:subject->resources-scans @work)))))) - (deftest generated-certified-projection-traces-match-cache-free-results-test (doseq [seed (range 1 41)] (let [values diff --git a/modules/eacl/test/eacl/cache/standard_lru_test.cljc b/modules/eacl/test/eacl/cache/standard_lru_test.cljc index 92651f5e2..201c9558a 100644 --- a/modules/eacl/test/eacl/cache/standard_lru_test.cljc +++ b/modules/eacl/test/eacl/cache/standard_lru_test.cljc @@ -60,18 +60,6 @@ (is (= {:found? true :value nil} (lru/lookup! store :nil))))) -(deftest lookup-holds-value-across-concurrent-policy-eviction-test - (let [store (lru/store 2) - held-value {:immutable [:answer 1]}] - (lru/put-if-absent! store :first held-value) - (lru/put-if-absent! store :second :second-value) - (let [held (lru/lookup! store :first)] - (lru/put-if-absent! store :third :third-value) - (is (= {:found? true :value held-value} held)) - ;; JVM Window TinyLFU may reject the new entry instead of selecting the - ;; exact strict-LRU victim. Retention policy never changes a held value. - (is (<= (lru/entry-count store) 2))))) - (deftest publication-peek-does-not-refresh-lru-test #?(:clj (let [store (lru/store 8)] @@ -248,25 +236,6 @@ (is (= {:found? false :value nil} (lru/lookup! store :key))))) -(deftest storage-never-invokes-a-loader-or-validator-test - (let [store (lru/store 2) - computations (atom 0) - validations (atom 0) - compute (fn [] (swap! computations inc) :computed) - value (compute)] - (is (= 1 @computations)) - (is (true? (lru/put-if-absent! store :key value))) - (let [{:keys [found? value]} (lru/lookup! store :key)] - (is found?) - (is (= :computed value)) - (is (= :valid - ((fn [candidate] - (swap! validations inc) - (if (= :computed candidate) :valid :invalid)) - value)))) - (is (= 1 @computations)) - (is (= 1 @validations)))) - #?(:clj (deftest concurrent-lookups-return-the-held-immutable-value-test (let [store (lru/store 64) @@ -294,7 +263,6 @@ (deftest concurrent-publication-computes-independently-and-never-overwrites-test (let [publisher-count 16 store (lru/store 32) - computations (atom 0) ready (java.util.concurrent.CountDownLatch. publisher-count) start (java.util.concurrent.CountDownLatch. 1) publishers @@ -302,10 +270,7 @@ (fn [publisher] (future ;; The completed value exists before entering cache storage. - (let [completed-value - ((fn [] - (swap! computations inc) - {:publisher publisher :completed true}))] + (let [completed-value {:publisher publisher :completed true}] (.countDown ready) (.await start) {:published? @@ -317,7 +282,6 @@ (let [results (mapv #(deref % 10000 ::timeout) publishers) winners (filterv :published? results) resident (:value (lru/lookup! store :answer))] - (is (= publisher-count @computations)) (is (= 1 (count winners))) (is (identical? (:value (first winners)) resident)) (is (= 1 (lru/entry-count store))))))) diff --git a/modules/eacl/test/eacl/cache_test.cljc b/modules/eacl/test/eacl/cache_test.cljc index 1571026e7..d82a2efb0 100644 --- a/modules/eacl/test/eacl/cache_test.cljc +++ b/modules/eacl/test/eacl/cache_test.cljc @@ -179,8 +179,8 @@ (defrecord CustomCursorId [value]) -(deftest concurrent-exact-hit-telemetry-counts-every-hit-test - #?(:clj +#?(:clj + (deftest concurrent-exact-hit-telemetry-counts-every-hit-test (let [store (cache/basis-cache {:max-entries 8}) semantic (semantic-key :concurrent-hot) workers 8 @@ -207,9 +207,7 @@ (is (zero? (:managed-hits stats))) (is (= expected (get-in stats [:subproblems :hits]))) (is (= expected - (get-in stats [:subproblems :answer-hits]))))) - :cljs - (is true))) + (get-in stats [:subproblems :answer-hits]))))))) (deftest rendered-pages-are-exact-read-through-values-test (let [store (cache/basis-cache {:max-entries 8}) @@ -352,9 +350,7 @@ (sorted-map-by #(compare %2 %1))))) (is (false? (cache/canonical-cursor-identity? - (sorted-set-by #(compare %2 %1)))))) - :cljs - (is true))) + (sorted-set-by #(compare %2 %1)))))))) (deftest cursor-identities-are-bounded-before-cache-key-construction-test (let [deep (nth (iterate vector "id") 40) @@ -624,7 +620,6 @@ (cache/resolve-basis! live-store (basis-context 1) semantic #(do (swap! calls inc) valid))))) - (is (= 1 @calls)) (is (= 1 @calls) "an accepted resident value is not recomputed per hit")) (let [source (cache/basis-cache {:max-entries 4}) diff --git a/modules/eacl/test/eacl/characterization_fixture_test.clj b/modules/eacl/test/eacl/characterization_fixture_test.clj index bf2447920..0e5112e2d 100644 --- a/modules/eacl/test/eacl/characterization_fixture_test.clj +++ b/modules/eacl/test/eacl/characterization_fixture_test.clj @@ -28,113 +28,6 @@ (sort-by :id) vec)) -(deftest formal-cljs-smoke-preserves-persistent-nrepl-executors-test - (let [runner - (slurp (repo/file "formal" "smoke" "cljs" "run")) - workflow - (slurp (repo/file ".github" "workflows" "formal.yml"))] - (is (str/includes? runner "cljs.build.api")) - (is (not (str/includes? runner "(cljs/-main"))) - (is (str/includes? - runner - "@(future :eacl.formal/agent-executor-alive)")) - (is (str/includes? workflow "cljs.build.api")) - (is (not (str/includes? workflow "(cljs/-main"))))) - -(deftest github-actions-provisions-temporal-tools-and-isolates-module-tests-test - (let [formal-workflow - (slurp (repo/file ".github" "workflows" "formal.yml")) - test-workflow - (slurp (repo/file ".github" "workflows" "test.yml")) - ^String temporal-job - (-> formal-workflow - (str/split #"\n temporal-models:\n" 2) - second - (str/split #"\n parity-corpus-and-mutations:\n" 2) - first)] - (testing "temporal mutation controls install their declared runtime" - (is (str/includes? temporal-job - "uses: DeLaGuardo/setup-clojure@")) - (is (str/includes? temporal-job "bb:")) - (is (< (.indexOf temporal-job "Set up Babashka") - (.indexOf temporal-job - "bin/formal apalache-mutation-control")))) - (testing "isolated modules exclude repository-global formal gates" - (is (str/includes? - test-workflow - "(?!eacl[.]formal[.]).*-test$"))))) - -(deftest advanced-cljs-build-and-extern-surface-are-wired-test - (let [workflow - (slurp (repo/file ".github" "workflows" "formal.yml")) - deps-cljs - (slurp (repo/file "formal" "smoke" "cljs" "deps.cljs")) - externs - (slurp - (repo/file - "formal" "smoke" "cljs" "eacl" "formal" - "generated_runtime.ext.js"))] - (is (str/includes? - workflow - "Run advanced-optimized CLJS production and differential suites")) - (is (<= 6 (count (re-seq #":optimizations :advanced" workflow)))) - (is (<= 6 (count (re-seq #":warnings-as-errors true" workflow)))) - (doseq [main ['eacl.formal.cljs-test-runner - 'eacl.datascript.cljs-test-runner - 'eacl.formal.empty-bundle-entry - 'eacl.formal.portable-kernel-bundle-entry - 'eacl.datascript.production-bundle-entry - 'eacl.formal.indexed-traversal-benchmark]] - (is (str/includes? workflow (str ":main '" main)) (str main))) - (is (str/includes? workflow - "node target/formal/cljs-advanced.js")) - (is (str/includes? workflow - "node target/formal/datascript-cljs-advanced.js")) - (is (str/includes? workflow - "eacl.formal.cljs-production-gate-test")) - (is (str/includes? deps-cljs - "eacl/formal/generated_runtime.ext.js")) - (doseq [property ["EaclFormal" - "create_RelationBinding" - "dtor_items" - "is_PlanCertified"]] - (is (str/includes? externs - (str "Object.prototype." property ";")) - property)))) - -(deftest formal-ci-isolates-and-stops-performance-nrepls-test - (let [workflow - (slurp (repo/file ".github" "workflows" "formal.yml")) - index - (fn [needle] - (.indexOf workflow needle)) - ordered-stages - ["Start heap-bounded generated-boundary nREPL" - "Gate portable CLJS indexed traversal scaling and ceiling" - "Restart heap-bounded nREPL for runtime performance suites" - "eacl.formal.verified-authority-suite/run-heavy!" - "eacl.formal.verified-authority-suite/run-nonbenchmark!" - "Restart heap-bounded nREPL for generated resource gates" - "Gate routing-certificate logical work and JVM allocation" - "Gate generated consistency-boundary overhead" - "Restart heap-bounded nREPL for recorded-baseline gates" - "Gate populated recursion against recorded v7 baselines" - "Gate Explorer enumeration against recorded v7 baselines" - "Stop CI nREPL"]] - (is (= 4 - (count - (re-seq - #"JAVA_TOOL_OPTIONS='-Xms128m -Xmx1024m'" - workflow)))) - (is (str/includes? workflow - "echo \"$!\" > target/formal/ci-nrepl.pid")) - (is (str/includes? workflow "if: always()")) - (is (str/includes? - workflow - "kill -KILL \"$nrepl_pid\" 2>/dev/null || true")) - (is (every? (comp not neg? index) ordered-stages)) - (is (apply < (map index ordered-stages))))) - (defn- source-definitions [path] (into diff --git a/modules/eacl/test/eacl/consistency_test.cljc b/modules/eacl/test/eacl/consistency_test.cljc index ccc7d1de8..f82e7f6c6 100644 --- a/modules/eacl/test/eacl/consistency_test.cljc +++ b/modules/eacl/test/eacl/consistency_test.cljc @@ -1,7 +1,6 @@ (ns eacl.consistency-test (:require [#?(:clj clojure.test :cljs cljs.test) :refer [deftest is]] - [eacl.backend.v8 :as backend] [eacl.causal-token :as causal-token] [eacl.consistency :as consistency] [eacl.spicedb.consistency :as public-consistency])) @@ -60,14 +59,11 @@ :revision 41 :exact-locator 41 :backend-snapshot-id {:database-id :test :basis-t 41}} - adapter-reads (atom {}) issued - (binding [backend/*backend-op-stats* adapter-reads] - (consistency/selected-basis-token - basis {:format-options format-options})) + (consistency/selected-basis-token + basis {:format-options format-options}) payload (causal-token/token-data format-options issued)] (is (= 41 (:revision payload))) (is (= 41 (:exact-locator payload))) (is (= "source" (:source-id payload))) - (is (= #uuid "56e42789-dff4-5066-96c9-d275736f47e2" (:source-lifecycle payload))) - (is (empty? @adapter-reads)))) + (is (= #uuid "56e42789-dff4-5066-96c9-d275736f47e2" (:source-lifecycle payload))))) diff --git a/modules/eacl/test/eacl/engine/scan_cache_test.cljc b/modules/eacl/test/eacl/engine/scan_cache_test.cljc index 5b91e613d..ad0822fd3 100644 --- a/modules/eacl/test/eacl/engine/scan_cache_test.cljc +++ b/modules/eacl/test/eacl/engine/scan_cache_test.cljc @@ -182,17 +182,63 @@ (is (= 2 (:entry-count stats))) (is (pos? (:scope-unavailable stats)))))) -(deftest shared-tier-keeps-the-longer-prefix-under-concurrent-extension-test - (let [tier (scan-cache/tier {:max-entries 16 :max-prefix 8}) - key [[:scope 17] (scan-cache/descriptor-key descriptor)] - store (:store tier) - short {:prefix [1 2 3] :exhausted? false} - long {:prefix [1 2 3 4 5 6] :exhausted? false}] - (is (true? (lru/put-if-absent! store key short))) - (is (true? (lru/replace-if! store key short long))) - (is (false? (lru/replace-if! store key short {:prefix [1 2 3 4] :exhausted? false})) - "a stale expected entry never overwrites the longer prefix") - (is (= long (:value (lru/lookup! store key)))))) +(deftest racing-deposits-leave-one-exact-prefix-in-the-shared-tier-test + ;; Two requests miss on the same resident state. The racing request runs to + ;; completion inside the outer request's adapter command, so its deposit + ;; lands between the outer request's lookup and the outer request's own + ;; deposit. `warm?` starts from a resident prefix (an extension) instead of + ;; an empty tier (a first deposit). + (doseq [warm? [true false] + [outer-limit racing-limit] [[1 3] [3 1]]] + (testing (str (if warm? "extension" "first deposit") ", outer limit " + outer-limit ", racing limit " racing-limit) + (let [tier (scan-cache/tier {:max-entries 16 :max-prefix 8}) + commands (atom []) + adapter (counting-inner {7 [1 2 3 4 5 6 7 8]} commands) + request (fn [inner] + (scan-cache/caching-fetch-fn + inner {:memo (scan-cache/memo) + :tier tier + :scope-fn (fn [relation-eid] + [:scope relation-eid])})) + command (fn [limit] + (cond-> (assoc descriptor :limit limit) + warm? (assoc :bound-eid 3))) + reply (fn [limit] + (vec (take limit (if warm? [4 5 6 7 8] [1 2 3 4 5 6 7 8])))) + deposit (fn [limit] + (into (if warm? [1 2 3] []) (reply limit))) + resident #(:value + (lru/lookup! + (:store tier) + (scan-cache/shared-key + [:scope 17] (scan-cache/descriptor-key descriptor)))) + racing-reply (atom nil)] + (when warm? + (is (= [1 2 3] ((request adapter) (assoc descriptor :limit 3)))) + (is (= {:prefix [1 2 3] :exhausted? false} (resident)))) + (let [before (count @commands) + outer (request + (fn [d] + (reset! racing-reply + ((request adapter) (command racing-limit))) + (adapter d)))] + (is (= (reply outer-limit) (outer (command outer-limit)))) + (is (= (reply racing-limit) @racing-reply)) + (is (= 2 (- (count @commands) before)) + "both requests missed and issued their own command") + (is (contains? #{{:prefix (deposit outer-limit) :exhausted? false} + {:prefix (deposit racing-limit) :exhausted? false}} + (resident)) + "the tier holds one request's exact prefix, never a mixture") + (when (< outer-limit racing-limit) + (is (= (deposit racing-limit) (:prefix (resident))) + "a deposit against a state that has since moved never overwrites the longer prefix")) + (is (= (reply 3) ((request adapter) (command 3))) + "a later request is answered exactly from whichever prefix stayed") + (is (<= (- (count @commands) before) 3) + "losing the race costs a later request at most one command") + (is (= {:prefix (deposit 3) :exhausted? false} (resident)))))))) (deftest unknown-operations-and-unbounded-limits-bypass-the-cache-test (with-ledger diff --git a/modules/eacl/test/eacl/formal/cache_strategy_adversarial_test.cljc b/modules/eacl/test/eacl/formal/cache_strategy_adversarial_test.cljc deleted file mode 100644 index bb7b6eaf7..000000000 --- a/modules/eacl/test/eacl/formal/cache_strategy_adversarial_test.cljc +++ /dev/null @@ -1,526 +0,0 @@ -(ns eacl.formal.cache-strategy-adversarial-test - "Finite falsification checks for the proposed cache-free/reference strategy. - - These are not a proof of the production implementation. They make the frame - assumptions executable, exhaust a small recursive graph, and retain mutants - for every key field whose omission produced a stale hit." - (:require [#?(:clj clojure.test :cljs cljs.test) - :refer [deftest is testing]] - [clojure.set :as set] - [eacl.authorization-oracle :as oracle] - [eacl.core :as eacl])) - -(defn- object - [type id] - (eacl/spice-object type id)) - -(def user-0 (object :user "u0")) -(def user-1 (object :user "u1")) -(def group-0 (object :group "g0")) -(def group-1 (object :group "g1")) -(def document (object :document "d0")) - -(def objects - [user-0 user-1 group-0 group-1 document]) - -(def rules - {[:group :view] - [:union - [:relation :member] - [:arrow :parent [:permission :view]]] - - [:document :view] - [:union - [:relation :reader] - [:arrow :group [:permission :view]]]}) - -(def relation-subject-types - {[:group :member] :user - [:group :parent] :group - [:document :reader] :user - [:document :group] :group - [:document :unrelated] :user}) - -(def possible-relationships - [(eacl/->Relationship user-0 :member group-0) - (eacl/->Relationship user-1 :member group-1) - (eacl/->Relationship group-0 :parent group-1) - (eacl/->Relationship group-1 :parent group-0) - (eacl/->Relationship user-0 :reader document) - (eacl/->Relationship user-1 :reader document) - (eacl/->Relationship group-0 :group document) - (eacl/->Relationship group-1 :group document) - (eacl/->Relationship user-1 :unrelated document)]) - -(defn- power-set - [values] - (reduce - (fn [subsets value] - (into subsets (map #(conj % value) subsets))) - [#{}] - values)) - -(defn- node-dependencies - [node] - (letfn [(walk-rule [resource-type rule seen] - (let [[operator & operands] rule] - (case operator - :relation - {:relations #{[resource-type (first operands)]} - :permissions #{}} - - :permission - (walk-permission - [resource-type (first operands)] - seen) - - :union - (reduce - (fn [result operand] - (merge-with - set/union - result - (walk-rule resource-type operand seen))) - {:relations #{} :permissions #{}} - operands) - - :arrow - (let [[via target] operands - subject-type - (get relation-subject-types - [resource-type via]) - target-result - (if subject-type - (walk-rule subject-type target seen) - {:relations #{} :permissions #{}})] - (update - target-result - :relations - conj - [resource-type via])) - - (throw - (ex-info - "Unknown adversarial rule operator." - {:operator operator - :rule rule}))))) - - (walk-permission [[resource-type permission :as permission-node] - seen] - (if (contains? seen permission-node) - {:relations #{} :permissions #{}} - (let [seen' (conj seen permission-node) - result - (walk-rule - resource-type - (get rules permission-node) - seen')] - (update - result - :permissions - conj - permission-node))))] - (walk-permission node #{}))) - -(def view-dependencies - (:relations (node-dependencies [:document :view]))) - -(defn- relationship-dependency - [relationship] - [(get-in relationship [:resource :type]) - (:relation relationship)]) - -(defn- project-relationships - [dependencies relationships] - (into - #{} - (filter - #(contains? - dependencies - (relationship-dependency %))) - relationships)) - -(defn- authorization-result - [relationships] - (->> (oracle/authorization-set - {:objects objects - :relationships relationships - :rules rules}) - (filter - (fn [[_subject permission resource]] - (and (= :view permission) - (= document resource)))) - (map first) - set)) - -(def exhaustive-states - (mapv - (fn [relationships] - {:relationships relationships - :projection - (project-relationships - view-dependencies - relationships) - :result (authorization-result relationships)}) - (power-set possible-relationships))) - -(defn- managed-key - [{:keys [query dependency-stamp result-layer]}] - [query dependency-stamp result-layer]) - -(defn- cache-namespace - [{:keys [semantic-abi adapter-abi lifecycle-generation - schema-generation]}] - [semantic-abi adapter-abi lifecycle-generation schema-generation]) - -(defn- command-traces - [commands length] - (if (zero? length) - [[]] - (for [prefix (command-traces commands (dec length)) - command commands] - (conj prefix command)))) - -(defn- authorization-at-version - [version] - (odd? version)) - -(defn- race-key - [versioned? version] - (if versioned? - [:query version] - :query)) - -(defn- cache-race-step - [versioned? state command] - (case command - :start - (update - state - :jobs - conj - {:version (:head state) - :value (authorization-at-version (:head state))}) - - :write - (update state :head inc) - - :publish - (if-let [job (first (:jobs state))] - (-> state - (assoc-in - [:cache (race-key versioned? (:version job))] - (:value job)) - (update :jobs #(vec (rest %)))) - state) - - :invalidate - (update - state - :cache - dissoc - (race-key versioned? (:head state))) - - :lookup - (let [key (race-key versioned? (:head state))] - (if (contains? (:cache state) key) - (update - state - :observations - conj - {:actual (get (:cache state) key) - :expected (authorization-at-version (:head state))}) - state)))) - -(defn- independent-computation-step - [join-mutant? state command] - (case command - :start - (let [version (:head state) - job {:computed-version version - :waiters [version]}] - (if (and join-mutant? (seq (:jobs state))) - (update-in state [:jobs 0 :waiters] conj version) - (update state :jobs conj job))) - - :write - (update state :head inc) - - :complete - (if-let [job (first (:jobs state))] - (-> state - (update - :observations - into - (map - (fn [waiter-version] - {:actual - (authorization-at-version - (:computed-version job)) - :expected - (authorization-at-version waiter-version)}) - (:waiters job))) - (update :jobs #(vec (rest %)))) - state))) - -(defn- stale-observation? - [state] - (some - (fn [{:keys [actual expected]}] - (not= actual expected)) - (:observations state))) - -(deftest dependency-frame-exhaustive-test - (testing "the complete relation projection determines the finite recursive result" - (is (= #{[:document :group] - [:document :reader] - [:group :member] - [:group :parent]} - view-dependencies)) - (is (= 512 (count exhaustive-states))) - (doseq [[projection states] - (group-by :projection exhaustive-states)] - (is (= 1 (count (set (map :result states)))) - (str "equal dependency projection changed authorization: " - (pr-str projection))))) - - (testing "an omitted target relation has a retained counterexample" - (let [mutant-dependencies - (disj view-dependencies [:group :member]) - collisions - (->> exhaustive-states - (group-by - #(project-relationships - mutant-dependencies - (:relationships %))) - vals - (filter - #(not= - 1 - (count (set (map :result %))))))] - (is (seq collisions) - "the missing-dependency mutant must be killed")))) - -(deftest versioned-publication-race-test - (let [base - {:query [:can? user-0 :view document] - :result-layer :decision} - old (assoc base :dependency-stamp 1) - current (assoc base :dependency-stamp 2) - late-publication {(managed-key old) false}] - (is (nil? (get late-publication (managed-key current))) - "an old computation published late is unreachable from a new epoch") - (is (false? - (get - {[:stable (:query base)] false} - [:stable (:query base)])) - "a stable-key invalidation mutant republishes the stale denial"))) - -(deftest publication-and-independent-computation-traces-exhaustive-test - (let [cache-traces - (command-traces - [:start :write :publish :invalidate :lookup] - 6) - initial-cache - {:head 0 :jobs [] :cache {} :observations []} - correct-cache-states - (map - #(reduce - (partial cache-race-step true) - initial-cache - %) - cache-traces) - mutant-cache-states - (map - #(reduce - (partial cache-race-step false) - initial-cache - %) - cache-traces) - computation-traces - (command-traces [:start :write :complete] 5) - initial-computation - {:head 0 :jobs [] :observations []} - independent-states - (map - #(reduce - (partial independent-computation-step false) - initial-computation - %) - computation-traces) - join-mutant-states - (map - #(reduce - (partial independent-computation-step true) - initial-computation - %) - computation-traces)] - (is (not-any? stale-observation? correct-cache-states) - "full versioned keys survive every bounded publication trace") - (is (some stale-observation? mutant-cache-states) - "stable-key publication retains a bounded stale trace") - (is (not-any? stale-observation? independent-states) - "each request-owned miss computes against its own selected version") - (is (some stale-observation? join-mutant-states) - "reintroducing a computation join couples a newer request to stale work"))) - -(deftest every-managed-frame-component-is-semantic-test - (let [namespace - {:semantic-abi :eacl-v8-build-a - :adapter-abi :datascript-1 - :lifecycle-generation :client-generation-a - :schema-generation :schema-a} - base - {:query [:can? user-0 :view document] - :dependency-stamp 1 - :result-layer :decision}] - (doseq [[label changed] - [[:semantic-abi - (assoc namespace - :semantic-abi - :eacl-v8-build-b)] - [:adapter-abi - (assoc namespace - :adapter-abi - :datascript-2)] - [:lifecycle-generation - (assoc namespace - :lifecycle-generation - :client-generation-b)] - [:schema - (assoc namespace - :schema-generation - :schema-b)]]] - (is (not= (cache-namespace namespace) - (cache-namespace changed)) - (str "cache namespace omitted " label))) - - (doseq [[label changed] - [[:query - (assoc base :query [:can? user-1 :view document])] - [:dependency - (assoc base - :dependency-stamp - 2)] - [:result-layer - (assoc base :result-layer :subject-set)]]] - (is (not= (managed-key base) - (managed-key changed)) - (str "managed key omitted " label)))) - - (testing "writer discipline is an explicit, indispensable assumption" - (let [before - {:query [:can? user-0 :view document] - :dependency-stamp 1 - :result-layer :decision - :content #{}} - dishonest-after - (assoc before - :content - #{(eacl/->Relationship - user-0 :reader document)})] - (is (= (managed-key before) - (managed-key dishonest-after)) - "an unstamped raw write is indistinguishable to an epoch cache") - (is (not= - (authorization-result (:content before)) - (authorization-result (:content dishonest-after))) - "the unstamped writer mutant changes authorization")))) - -(deftest scalar-current-transaction-stamp-finite-test - (testing "any relevant forward transaction raises the dependency maximum" - (doseq [stamps - (for [reader (range 4) - member (range 4) - parent (range 4)] - [reader member parent]) - changed-index (range (count stamps))] - (let [new-transaction 4 - changed - (assoc stamps changed-index new-transaction)] - (is (< (apply max stamps) - (apply max changed)))))) - - (testing "an unrelated write does not change the relevant maximum" - (is (= (apply max [3 1 2]) - (apply max [3 1 2])))) - - (testing "rewind can reuse stamps and therefore requires lifecycle expiry" - (let [before - {:query :q - :dependency-stamp 7 - :result-layer :decision} - after-rewind - (assoc before :content :different)] - (is (= (managed-key before) - (managed-key after-rewind)) - "managed cache does not support reset/force/history rewrite")))) - -(deftest managed-hit-renders-the-selected-snapshot-test - (let [entry - {:semantic-value true - :computation-snapshot 10} - selected-snapshot 11 - render - (fn [selected cached] - {:value (:semantic-value cached) - :selected-snapshot selected}) - stale-envelope-mutant - (fn [_selected cached] - {:value (:semantic-value cached) - :selected-snapshot - (:computation-snapshot cached)})] - (is (= {:value true :selected-snapshot 11} - (render selected-snapshot entry)) - "semantic hits are rendered against the selected snapshot") - (is (not= - (render selected-snapshot entry) - (stale-envelope-mutant selected-snapshot entry)) - "copying computation-snapshot metadata retains a mismatch"))) - -(deftest completed-cache-requires-canonical-snapshot-identity-test - (let [identity - (fn [lifecycle revision view-kind] - {:source-scope :source-a - :source-lifecycle lifecycle - :native-revision revision - :exact-locator revision - :view-kind view-kind - :adapter-fingerprint :adapter-v1 - :identity-contract :identity-v1}) - identity-100 (identity :lifecycle-a 100 :ordinary-exact) - exact-cache - {:entries {[identity-100 [:can? :q]] true}} - completed-cache-lookup - (fn [cache request] - (let [request-identity (:snapshot-identity request)] - (when (and (#{:current :at-exact-snapshot} (:mode request)) - (= :ordinary-exact (:view-kind request-identity))) - (get-in cache [:entries [request-identity (:query request)]]))))] - (is (true? (completed-cache-lookup - exact-cache - {:mode :at-exact-snapshot - :snapshot-identity identity-100 - :query [:can? :q]})) - "an authenticated exact request may reuse its identical snapshot") - (is (nil? (completed-cache-lookup - exact-cache - {:mode :current - :snapshot-identity - (identity :lifecycle-a 101 :ordinary-exact) - :query [:can? :q]})) - "a newer current snapshot cannot read the old exact generation") - (is (nil? (completed-cache-lookup - exact-cache - {:mode :at-exact-snapshot - :snapshot-identity - (identity :lifecycle-b 100 :ordinary-exact) - :query [:can? :q]})) - "numeric revision equality cannot cross lifecycle replacement") - (is (nil? (completed-cache-lookup - exact-cache - {:mode :at-exact-snapshot - :snapshot-identity - (identity :lifecycle-a 100 :filtered-view) - :query [:can? :q]})) - "an arbitrary view cannot masquerade as an ordinary exact snapshot"))) diff --git a/modules/eacl/test/eacl/formal/counterexample_replay_test.clj b/modules/eacl/test/eacl/formal/counterexample_replay_test.clj index e5cad4533..13be2cd25 100644 --- a/modules/eacl/test/eacl/formal/counterexample_replay_test.clj +++ b/modules/eacl/test/eacl/formal/counterexample_replay_test.clj @@ -10,7 +10,7 @@ :EACL-FORMAL-002 eacl.datomic.lookup-cache-test/recursive-cursors-resume-from-the-client-private-denotation-test :EACL-FORMAL-003 - eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + eacl.datomic.lookup-cache-test/cache-config-is-validated-test :EACL-FORMAL-004 eacl.datomic.cache-review-regressions-test/proofless-cursor-falls-back-to-exact-snapshot-test :EACL-FORMAL-005 @@ -20,7 +20,7 @@ :EACL-FORMAL-007 eacl.secure-format-test/canonical-portable-format-test :EACL-FORMAL-008 - eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + eacl.datomic.lookup-cache-test/cache-config-is-validated-test :EACL-FORMAL-009 eacl.formal.state-trace-differential-test/generated-cache-and-cursor-state-traces-across-jvm-adapters :EACL-FORMAL-010 @@ -30,15 +30,15 @@ :EACL-FORMAL-012 eacl.formal.production-kernel-test/generated-java-indexed-scan-response-boundary :EACL-FORMAL-013 - eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test :EACL-FORMAL-014 - eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test + eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test :EACL-FORMAL-015 eacl.datascript.snapshot-lifecycle-test/full-rotation-detaches-every-runtime-cache-child-test :EACL-FORMAL-016 - eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + eacl.subproblem-cache-test/publication-validation-runs-once-and-never-on-hit-test :EACL-FORMAL-017 - eacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test + eacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-test :EACL-FORMAL-018 eacl.datascript.snapshot-lifecycle-test/full-rotation-detaches-every-runtime-cache-child-test :EACL-FORMAL-019 @@ -59,26 +59,20 @@ eacl.formal.state-trace-differential-test/generated-stale-cursor-error-shape :EACL-FORMAL-027 eacl.backend.v8-test/runtime-guards-reject-negative-internal-eids-test - :EACL-FORMAL-028 - eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test :EACL-FORMAL-029 eacl.formal.counterexample-replay-test/counterexample-corpus-is-complete-and-closed-test :EACL-FORMAL-030 eacl.formal.production-kernel-test/generated-java-checks-linear-routing-certificates - :EACL-FORMAL-031 - eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test :EACL-FORMAL-032 eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test :EACL-FORMAL-033 eacl.datascript.contract-test/one-authority-is-the-only-production-engine-test - :EACL-FORMAL-034 - eacl.characterization-fixture-test/formal-cljs-smoke-preserves-persistent-nrepl-executors-test :EACL-FORMAL-035 eacl.characterization-fixture-test/generated-java-boundary-is-reflection-free-test :EACL-FORMAL-036 eacl.formal.production-kernel-test/generated-java-continues-pages-from-verified-lookahead :EACL-FORMAL-037 - eacl.datomic.impl.indexed-test/indexed-facade-has-no-shared-schema-cache-surface-test + eacl.datomic.api-contract-test/generated-authority-is-the-only-production-engine-test :EACL-FORMAL-038 eacl.verified-kernel-test/routing-certificate-result-is-bound-to-its-input :EACL-FORMAL-039 @@ -99,8 +93,6 @@ eacl.engine.stable-discovery-gate-test/fingerprint-is-invariant-under-schema-clause-order-test :EACL-FORMAL-047 eacl.datascript.keyset-recursion-test/order-perturbing-write-rejects-current-only-cursor-test - :EACL-FORMAL-048 - eacl.characterization-fixture-test/formal-ci-isolates-and-stops-performance-nrepls-test :EACL-FORMAL-049 eacl.datomic.recursive-cache-test/recursive-cursor-falls-back-to-exact-snapshot-after-relevant-write-test :EACL-FORMAL-050 @@ -119,10 +111,8 @@ eacl.datascript.impl-test/read-relationships-query-matrix-test :EACL-FORMAL-057 eacl.formal.page-window-bridge-test/generated-page-normalization-and-window-properties - :EACL-FORMAL-058 - eacl.formal.counterexample-replay-test/replay-entrypoint-does-not-eagerly-load-formal-only-oracles-test :EACL-FORMAL-059 - eacl.formal.counterexample-replay-test/clean-generated-javascript-contract-expectations-test + eacl.formal.production-kernel-test/generated-java-drives-production-recursive-pages :EACL-FORMAL-060 eacl.engine.physical-route-test/exhaustion-count-test :EACL-FORMAL-061 @@ -194,6 +184,16 @@ :EACL-FORMAL-099 eacl.datomic.self-counterexample-test/self-counterexample-replays-on-datomic-test}) +(def tooling-defects + "Ledger entries whose defect was in CI or test tooling, not in EACL. Nothing + in the product replays them: the gate that failed runs on every push, and + each entry's :closing-evidence names it." + #{:EACL-FORMAL-028 + :EACL-FORMAL-031 + :EACL-FORMAL-034 + :EACL-FORMAL-048 + :EACL-FORMAL-058}) + (defn- read-edn [path] (edn/read-string (slurp path))) @@ -243,49 +243,6 @@ (catch java.io.FileNotFoundException _ nil)))) -(deftest replay-entrypoint-does-not-eagerly-load-formal-only-oracles-test - (let [entrypoint (slurp (repo/file "bin" "formal"))] - (doseq [test-only-ns - ["eacl.lazy-merge-sort" - "eacl.backend.spi" - "eacl.engine.indexed"]] - (is (not (re-find - (re-pattern - (str - "\\(require '" - (java.util.regex.Pattern/quote test-only-ns) - " :reload\\)")) - entrypoint)) - (str - "the ordinary replay classpath must not eagerly load test-only " - test-only-ns))))) - -(deftest clean-generated-javascript-contract-expectations-test - (let [page-source - (slurp - (repo/file - "formal" "smoke" "cljs" "eacl" "formal" - "js_round_trip_test.cljs")) - production-source - (slurp - (repo/file - "formal" "smoke" "cljs" "eacl" "formal" - "production_kernel_test.cljs")) - vectors - (read-edn - (repo/file "formal" "cross-runtime" "vectors.edn"))] - (is (not (re-find #"\(contains\? request :(?:limit|cursor)\)" - page-source)) - "the generated RawPageRequest smoke must use only current v8 fields") - (is (= {:first-page [10 20] - :continuation-page [30]} - (:production-recursive-pages vectors)) - "the shared vector carries the stable first-discovery order") - (is (re-find - #":production-recursive-pages \(cross-runtime-vectors\)" - production-source) - "CLJS recursive pages must consume the shared JVM/JS vector"))) - (deftest counterexample-corpus-is-complete-and-closed-test (let [schema (read-edn (repo/file @@ -315,7 +272,8 @@ (str directory "/" artifact))) entry)) (entry-files))] - (is (= (set (keys regression-vars)) + (is (not-any? tooling-defects (keys regression-vars))) + (is (= (into (set (keys regression-vars)) tooling-defects) (set (map :id entries)))))) (deftest replay-every-minimized-regression-test diff --git a/modules/eacl/test/eacl/formal/dafny_cleanup_gate_test.clj b/modules/eacl/test/eacl/formal/dafny_cleanup_gate_test.clj index 413bfc15b..0a2efca96 100644 --- a/modules/eacl/test/eacl/formal/dafny_cleanup_gate_test.clj +++ b/modules/eacl/test/eacl/formal/dafny_cleanup_gate_test.clj @@ -4,31 +4,6 @@ [clojure.test :refer [deftest is testing]] [eacl.test-support.repo :as repo])) -(def active-source-roots - [(repo/file "formal" "dafny") - (repo/file "formal" "smoke" "cljs") - (repo/file "formal" "smoke" "js") - (repo/file "modules" "eacl" "src")]) - -(def retired-markers - ["module Pagination" - "CursorBoundRebase" - "RebaseCursorBound" - "PaginateRelationshipContinuation" - "datatype AfterCursor" - "RenderBackwardPage" - ":backward-page"]) - -(defn- file-path [^java.io.File file] - (.getPath file)) - -(defn- active-source-file? [^java.io.File file] - (let [path (.getPath file)] - (and (.isFile file) - (not (str/includes? path "node_modules")) - (some #(str/ends-with? path %) - [".clj" ".cljc" ".cljs" ".dfy" ".mjs" ".cjs" ".html"])))) - (defn- entry-point-exists? [entry-point] (cond (and (symbol? entry-point) (namespace entry-point)) @@ -101,18 +76,6 @@ entry-point))) (is (seq dafny)))))) -(deftest retired-dafny-surface-is-absent-test - (is (not (.exists (io/file (repo/file "formal" "dafny") - "Pagination.dfy")))) - (doseq [file (mapcat file-seq active-source-roots) - :when (active-source-file? file)] - ;; One read per file; the marker loop previously re-slurped every - ;; file once per marker. - (let [source (slurp file)] - (doseq [marker retired-markers] - (is (not (str/includes? source marker)) - (str marker " remains in " (file-path file))))))) - ;;; Induction policy. Dafny 4.11 can verify a false lemma by induction on a ;;; sequence parameter, whether automatic lemma induction chose it or an ;;; `{:induction x}` attribute requested it (repro and analysis in the diff --git a/modules/eacl/test/eacl/operator_engine/counterexamples_test.clj b/modules/eacl/test/eacl/operator_engine/counterexamples_test.clj index 143257864..e8cf365ad 100644 --- a/modules/eacl/test/eacl/operator_engine/counterexamples_test.clj +++ b/modules/eacl/test/eacl/operator_engine/counterexamples_test.clj @@ -1,7 +1,6 @@ (ns eacl.operator-engine.counterexamples-test (:require [clojure.edn :as edn] - [clojure.set :as set] - [clojure.test :refer [deftest is testing]] + [clojure.test :refer [deftest is]] [eacl.operator-engine.oracle :as oracle] [eacl.test-support.repo :as repo])) @@ -16,66 +15,13 @@ [id] (first (filter #(= id (:id %)) (fixtures)))) -(defn- relation-member? - [snapshot resource relation subject] - (contains? - (:relationships snapshot) - {:resource resource :relation relation :subject subject})) - -(defn- active-as-false-mutant - [snapshot evaluation-order] - (let [memo (atom {})] - (letfn [(evaluate-expression [resource-type resource subject active expression] - (case (first expression) - :relation - (relation-member? - snapshot resource (second expression) subject) - :permission - (evaluate-permission - [resource-type (second expression)] resource subject active) - :union - (boolean - (some #(evaluate-expression - resource-type resource subject active %) - (rest expression))) - :intersection - (every? #(evaluate-expression - resource-type resource subject active %) - (rest expression)) - :exclusion - (and (evaluate-expression - resource-type resource subject active - (second expression)) - (not (evaluate-expression - resource-type resource subject active - (nth expression 2)))))) - (evaluate-permission [permission-key resource subject active] - (let [state [permission-key resource subject]] - (if (contains? @memo state) - (get @memo state) - (if (contains? active state) - false - (let [result - (evaluate-expression - (first permission-key) resource subject - (conj active state) - (get-in snapshot [:permissions permission-key]))] - (swap! memo assoc state result) - result)))))] - (mapv - (fn [[permission-key resource subject]] - (evaluate-permission permission-key resource subject #{})) - evaluation-order)))) - (deftest active-recursion-is-not-completed-false-test - (let [{:keys [snapshot evaluation-order query expected]} + (let [{:keys [snapshot query expected]} (fixture :active-recursion-as-false) evaluation (oracle/evaluate-stratified snapshot)] (is (= expected (oracle/evaluated-check? - evaluation (:subject query) (:permission query) (:resource query)))) - (is (= [true false] - (active-as-false-mutant snapshot evaluation-order))))) + evaluation (:subject query) (:permission query) (:resource query)))))) (deftest every-intersection-premise-is-required-test (let [{:keys [snapshot query expected]} @@ -94,17 +40,6 @@ (:subject query)) (rest expression))))))) -(deftest incomplete-exclusion-right-is-not-absence-test - (let [{:keys [left right expected]} - (fixture :partial-right-side-absence) - mutant-result - (if (and (= :completed-true left) - (not= :completed-true right)) - :grant - :deny)] - (is (= :propagate-incomplete expected)) - (is (= :grant mutant-result)))) - (deftest exclusion-operands-are-directed-test (let [{:keys [snapshot query expected]} (fixture :swapped-exclusion-operands) @@ -119,61 +54,6 @@ (oracle/check? swapped (:subject query) (:permission query) (:resource query)))))) -(deftest cursor-progress-stops-at-logical-boundary-test - (let [{:keys [physical-batch returned expected-cursor-boundary - expected-resume]} - (fixture :cursor-advanced-through-batch-overread) - correct-boundary (peek returned) - correct-resume - (vec (rest (drop-while #(not= correct-boundary %) physical-batch))) - mutant-boundary (peek physical-batch) - mutant-resume - (vec (rest (drop-while #(not= mutant-boundary %) physical-batch)))] - (is (= expected-cursor-boundary correct-boundary)) - (is (= expected-resume correct-resume)) - (is (not= expected-resume mutant-resume)))) - -(deftest typed-identity-is-part-of-every-join-key-test - (let [{:keys [left right expected]} - (fixture :wrong-typed-id-join-identity) - mutant - (set - (for [left-value left - right-value right - :when (= (second left-value) (second right-value))] - left-value))] - (testing "correct typed intersection" - (is (= expected (set/intersection left right)))) - (testing "the id-only mutant grants" - (is (= #{[:user "same"]} mutant))))) - -(deftest arrow-catalog-must-cover-every-intermediate-test - (let [{:keys [resource subject intermediate catalog relationships expected]} - (fixture :incomplete-arrow-object-catalog) - relation? (fn [r rel s] - (contains? relationships - {:resource r :relation rel :subject s})) - catalog-mutant - (boolean - (some #(and (relation? resource :parent %) - (relation? % :member subject)) - catalog)) - exact-existential - (and (relation? resource :parent intermediate) - (relation? intermediate :member subject))] - (is (= expected exact-existential)) - (is (false? catalog-mutant)))) - -(deftest cache-invalidation-is-by-relation-not-dependency-sign-test - (let [{:keys [dependencies changed expected-invalidated]} - (fixture :cache-write-sign-mismatch) - relation-invalidated? - (boolean - (some #(= (:relation %) (:relation changed)) dependencies)) - signed-mutant-invalidated? (contains? dependencies changed)] - (is (= expected-invalidated relation-invalidated?)) - (is (false? signed-mutant-invalidated?)))) - (deftest forged-scc-components-cannot-hide-negative-cycle-test (let [{:keys [snapshot forged-components expected-error]} (fixture :unchecked-scc-certificate) diff --git a/modules/eacl/test/eacl/relay_test.cljc b/modules/eacl/test/eacl/relay_test.cljc index f6e70df4c..fc82fc0cc 100644 --- a/modules/eacl/test/eacl/relay_test.cljc +++ b/modules/eacl/test/eacl/relay_test.cljc @@ -720,38 +720,6 @@ (is (= :eacl.consistency/basis-conflict (:type data))) (is (= :cursor (:source data))))) -(deftest recursive-snapshot-continuation-does-not-rebase-test - (let [original (adapter 1 nil true) - current (adapter 2 nil true) - recursive-page - (assoc-in - lookup-page - [:page-info :end-cursor] - {:kind :lookup-eid - :frontier-direction :asc - :result-eid "document-1"}) - first-page - (relay/externalize-page - original - {:snapshot-semantic-identity (basis-identity 1)} - :lookup-resources lookup-query recursive-page) - data - (try - (relay/prepare-page-query - current - {:cursor-consistency-mode :minimize-latency - :authorization-target-kind :snapshot - :snapshot-semantic-identity (basis-identity 2)} - :lookup-resources - (assoc lookup-query - :after - (get-in first-page [:page-info :end-cursor]))) - nil - (catch #?(:clj clojure.lang.ExceptionInfo :cljs :default) error - (ex-data error)))] - (is (= :eacl.consistency/basis-conflict (:type data))) - (is (= :cursor (:source data))))) - (deftest expired-cursor-reaches-the-kernel-decision-test ;; cursor-dependency-validity: the TTL check result is a computed input of ;; the verified continuation decision. The expired token flows TO the @@ -843,7 +811,7 @@ :result-eid "document-1"} (get-in prepared [:query :after])) "the old authenticated transport is internalized to its exact boundary") - (is (not (contains? (:cursor-context (:opts prepared)) :exp)) + (is (false? (:expiring-cursor-input? prepared)) "elapsed age far beyond five minutes is irrelevant without an explicit TTL"))) (deftest one-page-builds-one-snapshot-context-test diff --git a/modules/eacl/test/eacl/secure_format_test.cljc b/modules/eacl/test/eacl/secure_format_test.cljc index ad0ed9106..d64a51164 100644 --- a/modules/eacl/test/eacl/secure_format_test.cljc +++ b/modules/eacl/test/eacl/secure_format_test.cljc @@ -387,21 +387,6 @@ (:reason (error-data #(token/token-data options "17"))))))) -(deftest source-lifecycle-is-bounded-portable-canonical-data-test - (is (= :invalid-source-lifecycle - (:reason - (error-data - #(token/validate-source-lifecycle! - {:invalid (fn [])}))))) - (is (= :invalid-source-lifecycle - (:reason - (error-data - #(token/validate-source-lifecycle! - {:oversized (apply str - (repeat - token/maximum-scope-characters - "x"))})))))) - (deftest authenticated-portable-cursor-test (let [value {:v 8 :edge {:kind :lookup-eid} :position [1 "a"]} encoded (cursor/cursor->token value options)] @@ -803,25 +788,6 @@ (is (= :eacl/invalid-config (:type data))) (is (= :max-entries (:option data)))))) -(deftest encrypted-cursors-reuse-client-private-key-context-test - (let [codec-cache (cursor/codec-cache {:max-entries 4}) - cached-options (assoc options :cursor-codec-cache codec-cache) - work (atom {})] - (binding [cursor/*codec-work* work] - (is (string? - (cursor/cursor->token - {:v 10 :scope :one :edge {:kind :lookup-eid :value 1}} - cached-options))) - (is (string? - (cursor/cursor->token - {:v 10 :scope :two :edge {:kind :lookup-eid :value 2}} - cached-options)))) - (is (= 2 (:encode-calls @work))) - (is (= 1 (:key-context-builds @work)) - "the first cursor derives and encodes the configured key context") - (is (= 1 (:key-context-cache-hits @work)) - "the next distinct cursor reuses key derivation without reusing a token"))) - (deftest encrypted-cursor-key-context-cache-retains-hot-context-test (let [kids (mapv #(keyword (str "key-" %)) (range 17)) keyring diff --git a/modules/eacl/test/eacl/subproblem_cache_test.cljc b/modules/eacl/test/eacl/subproblem_cache_test.cljc index ba3c7a2ed..0d7f4af63 100644 --- a/modules/eacl/test/eacl/subproblem_cache_test.cljc +++ b/modules/eacl/test/eacl/subproblem_cache_test.cljc @@ -152,8 +152,8 @@ (is (:cached? false-hit)) (is (false? (:value false-hit)))))) -(deftest concurrent-lookup-telemetry-counts-every-hit-test - #?(:clj +#?(:clj + (deftest concurrent-lookup-telemetry-counts-every-hit-test (let [store (subproblem/store small-options) key (storage-key :answer :concurrent-hot) workers 8 @@ -177,9 +177,7 @@ (is (= expected (:hits metrics))) (is (= expected (:answer-hits metrics))) (is (zero? (:lookup-misses metrics))) - (is (zero? (:denotation-hits metrics))))) - :cljs - (is true))) + (is (zero? (:denotation-hits metrics))))))) (deftest invalid-values-never-publish-test (let [store (subproblem/store small-options)] @@ -580,18 +578,25 @@ (is (= :eacl/cache-snapshot-incompatible (failure-type one-entry #(throw (ex-info "invalid" {:entry %}))))) (is (= :eacl/cache-snapshot-incompatible - (failure-type + (failure-type (assoc one-entry :entry-count 2) (constantly true))) + "the declared entry count must match the entries") + (let [page-snapshot + (fn [size] {:format subproblem/snapshot-format :entries [{:tier :answer - :key (storage-key :answer :large-page)} - :value - {:format :eacl.cache/completed-answer-v3 - :value (page 1001) - :cache-basis {:basis 1} - :computed-revision 1 - :computed-exact-locator 1}] - :entry-count 1} - (constantly true)))))) + :key (storage-key :answer :large-page) + :value + {:format :eacl.cache/completed-answer-v3 + :value (page size) + :cache-basis {:basis 1} + :computed-revision 1 + :computed-exact-locator 1}}] + :entry-count 1})] + ;; The two snapshots differ only in page size, so the rejection is the + ;; page guard and not an earlier structural check. + (is (nil? (failure-type (page-snapshot 1000) (constantly true)))) + (is (= :eacl/cache-snapshot-incompatible + (failure-type (page-snapshot 1001) (constantly true))))))) (deftest removed-projection-and-weight-options-fail-closed-test (doseq [removed-option [:projection-max-entries diff --git a/modules/eacl/test/eacl/subproblem_maintenance_test.cljc b/modules/eacl/test/eacl/subproblem_maintenance_test.cljc index 0039c4d81..c7f77a1bd 100644 --- a/modules/eacl/test/eacl/subproblem_maintenance_test.cljc +++ b/modules/eacl/test/eacl/subproblem_maintenance_test.cljc @@ -1,6 +1,6 @@ (ns eacl.subproblem-maintenance-test "Maintenance invariants now delegated to the standard LRU implementation." - (:require [clojure.test :refer [deftest is testing]] + (:require [clojure.test :refer [deftest is]] [eacl.cache.key :as cache-key] [eacl.subproblem-cache :as sub])) @@ -25,12 +25,3 @@ store :denotation (storage-key [:churn (dec n)])))) (is (= {:entries capacity :max-entries capacity} (get-in (sub/stats store) [:tiers :denotation]))))) - -(deftest no-homegrown-policy-state-is-exposed-test - (let [store (sub/store {:denotation-max-entries 2}) - tier-stats (get-in (sub/stats store) [:tiers :denotation])] - (testing "capacity is an entry count, not a logical byte estimate" - (is (= #{:entries :max-entries} (set (keys tier-stats)))) - (is (nil? (:weight tier-stats))) - (is (nil? (:lru-records tier-stats))) - (is (nil? (:eviction-probes (sub/stats store))))))) diff --git a/modules/eacl/test/eacl/verified_kernel_test.cljc b/modules/eacl/test/eacl/verified_kernel_test.cljc index 93d8cb696..40faa28c8 100644 --- a/modules/eacl/test/eacl/verified_kernel_test.cljc +++ b/modules/eacl/test/eacl/verified_kernel_test.cljc @@ -163,18 +163,6 @@ (->FunctionKernel (fn [_ _] expected))} :consistency-validation input)))))) - (testing "snapshot absence and a malformed present value remain distinct" - (let [absent {:kind :exact - :selection-present? false - :selected-adapter? false - :same-source-scope? false - :revision-satisfied? false} - malformed (assoc absent - :selection-present? true)] - (is (= :exact-snapshot-unavailable - (expected-consistency-validation absent))) - (is (= :invalid-selected-adapter - (expected-consistency-validation malformed))))) (testing "unknown fields, impossible observations, and lying kernels fail" (let [plan {:mode :minimize-latency :capability-supported? true} diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/.openspec.yaml b/openspec/changes/2026-10-04-delete-tautological-tests/.openspec.yaml new file mode 100644 index 000000000..f98e139fb --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/.openspec.yaml @@ -0,0 +1,2 @@ +schema: spec-driven +created: 2026-10-04 diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/design.md b/openspec/changes/2026-10-04-delete-tautological-tests/design.md new file mode 100644 index 000000000..9bcd85231 --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/design.md @@ -0,0 +1,69 @@ +# Design + +## Context + +See proposal.md for motivation. The counterexample replay test requires a +regression var for every ledger entry, so a test that is some entry's +regression var has to be replaced before it can go. + +## Goals / Non-Goals + +**Goals:** + +- Every regression var is a test that can fail when behavior changes. +- No ledger entry loses its record: fixture, expected result and README stay. + +**Non-Goals:** + +- Self-tests of oracles, generators and gates that other tests rely on. +- Lints that enforce a rule over current sources: the Dafny induction policy, + the relationship-literal audit, the public source closure. +- Pins of the persisted storage format. +- The `formal/` tree, apart from namespace lists that name a deleted file. + +## Decisions + +**What counts as tautological.** A test is deleted when every assertion in it +is one of these: + +- a removed var, namespace, resource, attribute or key is absent; +- a script, workflow, source file or dependency file contains or lacks literal + text; +- a model or "mutant" defined in the test file behaves as written. + +Alternative considered: also delete self-tests of test-tree code. Rejected, +because those tests can fail and differential tests depend on the code they +check. + +**Removed-option tests stay.** They call the public constructor and assert the +rejection, which is behavior. + +**Replacing a regression var.** Where the defective path was deleted, the entry +points at a test of what replaced it. + +| Entries | Replacement regression | +|---|---| +| 003, 008 | a caller-supplied cache provider is rejected at construction | +| 013, 014, 017 | concurrent publishers compute independently and one publication wins | +| 016 | lookup is read-only; validation runs once, at publication | +| 037 | the Datomic client's decision kernel is the generated authority | +| 059 | the JVM smoke test that consumes the shared cross-runtime page vector | + +**Tooling defects.** Entries 028, 031, 034, 048 and 058 record defects in CI +scripts or test harnesses. Their regressions were text checks of those scripts. +The replay test gains a `tooling-defects` set, and the corpus check requires +every entry to be in that set or to have a regression var, never both. + +Alternative considered: point those entries at an unrelated passing test so +that one map covers the ledger. Rejected, because that is a regression in name +only. + +## Risks / Trade-offs + +- [A deleted name comes back unnoticed] → Reintroduced dead code is a review + matter and shows in the public source closure; a test that lists names does + not test what the code does. +- [A replacement regression is narrower than the original defect] → Each + replacement is taken from the entry's own `:fix` text, and the ledger keeps + the original witness. +- [A CI script regresses] → The gate it runs fails on the next push. diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/proposal.md b/openspec/changes/2026-10-04-delete-tautological-tests/proposal.md new file mode 100644 index 000000000..e688b1c8c --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/proposal.md @@ -0,0 +1,46 @@ +# Proposal + +## Why + +Some tests cannot detect a defect in EACL. They assert that a removed name is +still absent, restate the text of a script or workflow, or exercise a model +defined in the test file. Two requirements ask for such tests, and the +counterexample ledger closes thirteen entries with them. Assurance should come +from tests of behavior through the public API. + +## What Changes + +- Delete eighteen tests of those three kinds, and six assertions of the same + kind inside five tests that stay. +- Point each ledger entry that those tests closed at a test that executes the + behavior that replaced the defective path: rejection of caller-supplied cache + providers, independent concurrent publication, read-only lookup, and the + single production authority. +- Record five ledger entries whose defect was in CI or test tooling as closed + by the gate that failed, without a product regression. +- Stop requiring negative source assertions for deleted paths. + +## Capabilities + +### New Capabilities + +None. + +### Modified Capabilities + +- `implementation-simplicity-and-performance`: "Simplicity and performance + evidence is certification-linked" no longer requires negative source + assertions for deleted paths, and rules them out. +- `formally-verified-authorization-engine`: "Counterexample-driven bug + discovery" says what counts as a retained regression, and how an entry is + closed when the defective path was deleted or the defect was in tooling. + +## Impact + +- Tests under `modules/*/test` and `src-build`. +- The `regression-vars` map and the corpus check in + `eacl.formal.counterexample-replay-test`. +- `formal/counterexamples/*/entry.edn` for the affected entries. +- Namespace lists in the DataScript ClojureScript runner, the two + verified-authority suites, and `.github/workflows/formal.yml`. +- No production code. diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/specs/formally-verified-authorization-engine/spec.md b/openspec/changes/2026-10-04-delete-tautological-tests/specs/formally-verified-authorization-engine/spec.md new file mode 100644 index 000000000..31d589de9 --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/specs/formally-verified-authorization-engine/spec.md @@ -0,0 +1,25 @@ +## MODIFIED Requirements + +### Requirement: Counterexample-driven bug discovery +The repository SHALL provide coherent generators and temporal models that search direct, recursive, forward, reverse, cursor, cache, restore, reset, branch, retention, tampering, and provider-failure behavior. Every discovered mismatch or invariant violation SHALL be minimized, reproducible, classified, and retained as a regression before it is considered resolved. A retained regression SHALL execute the code that carried the defect, or the behavior that replaced it, and SHALL fail if the defect returns. A test that asserts only that a name is absent, that a file contains or lacks literal text, or that a model defined in the test file behaves as written is not a regression. + +#### Scenario: Differential mismatch +- **WHEN** the formal semantics, verified kernel, legacy engine, public API, or supported runtime disagree +- **THEN** the run fails with a reproducible seed and emits or records the smallest available schema, graph, request, and state trace + +#### Scenario: Model-checker violation +- **WHEN** temporal exploration violates a cache, cursor, or causal-history invariant +- **THEN** the counterexample trace is translated into a failing executable regression test before the implementation is corrected + +#### Scenario: Security-significant defect +- **WHEN** a counterexample permits a false grant, stale authorization, cross-scope cursor, or mixed-snapshot result +- **THEN** the bug ledger records affected versions/backends, security impact, root cause, fix, and closing proof/test + +#### Scenario: The defective path was deleted +- **WHEN** the code path that carried a recorded defect no longer exists +- **THEN** the ledger entry's regression is a test of the public behavior that replaced that path + +#### Scenario: The defect was in tooling +- **WHEN** a ledger entry records a defect in CI or test tooling rather than in EACL +- **THEN** the entry names the gate that failed as its closing evidence +- **AND** the entry has no product regression diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/specs/implementation-simplicity-and-performance/spec.md b/openspec/changes/2026-10-04-delete-tautological-tests/specs/implementation-simplicity-and-performance/spec.md new file mode 100644 index 000000000..9e819f1db --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/specs/implementation-simplicity-and-performance/spec.md @@ -0,0 +1,25 @@ +## MODIFIED Requirements + +### Requirement: Simplicity and performance evidence is certification-linked + +Every structural inventory and non-regression result MUST be mapped into the +implementation-conformance ledger and reproducible certification bundle with +source closure and digests. Measured results MUST carry the exact production +artifact digest they test. A deleted path MUST NOT be pinned by a test that +asserts only that a name is absent, or that a file contains or lacks literal +text. The behavior that replaced the path SHALL be asserted through the public +API. + +#### Scenario: Evidence targets a different binary or source closure + +- **WHEN** simplicity or performance evidence does not match the candidate + production artifact and source-closure digest +- **THEN** the conformance gate rejects the evidence as stale +- **AND** prospective external certification remains unavailable + +#### Scenario: A path is deleted + +- **WHEN** a code path, option, or storage attribute is deleted +- **THEN** no test asserts its absence by name or by searching source text +- **AND** a test of the public behavior that replaced it fails if that + behavior regresses diff --git a/openspec/changes/2026-10-04-delete-tautological-tests/tasks.md b/openspec/changes/2026-10-04-delete-tautological-tests/tasks.md new file mode 100644 index 000000000..5e055e793 --- /dev/null +++ b/openspec/changes/2026-10-04-delete-tautological-tests/tasks.md @@ -0,0 +1,17 @@ +# Tasks + +## 1. Delete tests that the ledger does not name + +- [x] 1.1 Delete the absence tests (raw entry points, retired schema attributes, retired Dafny markers, exposed policy state) and the six absence assertions inside tests that stay; verify the edited namespaces load and pass +- [x] 1.2 Delete the text tests of dependency files and spec files, with the probe only they used; verify no definition is left unused + +## 2. Delete tests that the ledger names + +- [x] 2.1 Retarget entries 003, 008, 013, 014, 016, 017, 037 and 059 in `regression-vars` and in each entry's `:closing-evidence`; verify the corpus check passes +- [x] 2.2 Add `tooling-defects` for 028, 031, 034, 048 and 058 and require every entry to be in exactly one of the two; verify the corpus check passes, and fails when an entry is in neither +- [x] 2.3 Delete the audit, facade, launcher, workflow, entrypoint and generated-JavaScript text tests and the in-test cache model, and remove their namespaces from the runner lists; verify strict replay resolves every regression var + +## 3. Verify + +- [x] 3.1 Run the CI battery, the DataScript ClojureScript suite, strict counterexample replay and the verified-authority suites; verify zero failures +- [x] 3.2 Compare production coverage of the battery before and after; record any line that is no longer executed diff --git a/src-build/eacl/build/config_test.clj b/src-build/eacl/build/config_test.clj index 526769144..9301a0b01 100644 --- a/src-build/eacl/build/config_test.clj +++ b/src-build/eacl/build/config_test.clj @@ -106,34 +106,6 @@ (get-in datahike-dependencies ['org.replikativ/datahike :exclusions]))))) -(deftest standard-cache-source-dependencies-are-pinned - (let [root-dependencies (:deps (edn/read-string (slurp "deps.edn"))) - core-dependencies - (:deps (edn/read-string (slurp "modules/eacl/deps.edn"))) - datahike-dependencies - (:deps (edn/read-string - (slurp "modules/eacl-datahike/deps.edn"))) - backend-probe-dependencies - (:deps - (edn/read-string - (slurp "exploration/stable-discovery/backend-probes/deps.edn"))) - cljs-cache - {:git/url "https://github.com/theronic/cljs-cache.git" - :git/sha "4143cc036446a47f0c6dfd9f8dde90363835051c"}] - (doseq [dependencies [root-dependencies core-dependencies]] - (is (= {:mvn/version "3.2.4"} - (get dependencies - 'com.github.ben-manes.caffeine/caffeine))) - (is (not (contains? dependencies 'org.clojure/core.cache))) - (is (= cljs-cache - (get dependencies 'com.github.theronic/cljs-cache)))) - (doseq [dependencies [root-dependencies - datahike-dependencies - backend-probe-dependencies]] - (is (= ['com.github.pkpkpk/cljs-cache] - (get-in dependencies - ['org.replikativ/datahike :exclusions])))))) - (deftest production-module-files-use-dev-eacl-coordinates (is (true? (module/assert-module-coordinates!)))) diff --git a/src-build/eacl/build/module_test.clj b/src-build/eacl/build/module_test.clj index 86ecb0c3d..c68bb40fe 100644 --- a/src-build/eacl/build/module_test.clj +++ b/src-build/eacl/build/module_test.clj @@ -124,9 +124,3 @@ (is (not (contains? (set (:entries failure)) owned))))) (finally (b/delete {:path (.getPath directory)}))))) - -(deftest core-artifact-does-not-require-retired-cache-policy-bytecode - (is (contains? module/required-core-entries - "AcyclicEngine/__default.class")) - (is (not (contains? module/required-core-entries - "CurrentCache/__default.class")))) diff --git a/src-build/eacl/build/release_test.clj b/src-build/eacl/build/release_test.clj index 624eaba7d..64c6d23ce 100644 --- a/src-build/eacl/build/release_test.clj +++ b/src-build/eacl/build/release_test.clj @@ -5,14 +5,6 @@ [eacl.build.module :as module] [eacl.build.release :as release])) -(deftest release-workflow-maps-the-configured-environment-secrets - (let [workflow (slurp ".github/workflows/release.yml")] - (is (string/includes? workflow "secrets.CLOJARS_USERNAME")) - (is (string/includes? workflow "secrets.CLOJARS_DEPLOY_TOKEN")) - (is (not (string/includes? workflow "secrets.CLOJURE_"))) - (is (string/includes? workflow "run: clojure -X:deploy")) - (is (string/includes? workflow "EACL_JAVA_RELEASE: '25'")))) - (deftest release-build-propagates-one-explicit-java-target (let [builds (atom [])] (with-redefs [module/assert-module-coordinates! (constantly true) diff --git a/src-build/eacl/build/source_prep_test.clj b/src-build/eacl/build/source_prep_test.clj deleted file mode 100644 index d3b9dbb21..000000000 --- a/src-build/eacl/build/source_prep_test.clj +++ /dev/null @@ -1,43 +0,0 @@ -(ns eacl.build.source-prep-test - (:require [clojure.edn :as edn] - [clojure.java.io :as io] - [clojure.test :refer [deftest is testing]])) - -(defn- repository-root - [] - (loop [candidate (.getCanonicalFile (io/file "."))] - (cond - (.isDirectory (io/file candidate "modules" "eacl")) - candidate - - (nil? (.getParentFile candidate)) - (throw - (ex-info "Could not locate the EACL repository root." - {:start (.getCanonicalPath (io/file "."))})) - - :else - (recur (.getParentFile candidate))))) - -(deftest source-dependency-resolution-never-prepares-formal-tools - (let [root (repository-root) - deps - (edn/read-string - (slurp (io/file root "modules" "eacl" "deps.edn"))) - build-source - (slurp (io/file root "modules" "eacl" "build.clj")) - java-build-script - (slurp (io/file root "formal" "smoke" "java" "run"))] - (testing "tools.deps has no automatic preparation hook" - (is (nil? (:deps/prep-lib deps))) - (is (= ["src" - "target/generated/java/classes" - "target/generated/browser"] - (:paths deps)))) - (testing "source preparation remains an explicit build function" - (is (re-find #"\(defn prep" build-source)) - (is (re-find #"Build and stage the generated JVM and browser runtimes" - build-source))) - (testing "Java 25 is the default but source preparation accepts an override" - (is (re-find #"EACL_JAVA_RELEASE:-25" java-build-script)) - (is (re-find #"javac --release \"\$java_release\"" - java-build-script))))) diff --git a/src-build/eacl/release_guard_test.clj b/src-build/eacl/release_guard_test.clj index 63dd7d123..f495a0c23 100644 --- a/src-build/eacl/release_guard_test.clj +++ b/src-build/eacl/release_guard_test.clj @@ -1,6 +1,5 @@ (ns eacl.release-guard-test - (:require [clojure.string :as string] - [clojure.test :refer [deftest is testing]] + (:require [clojure.test :refer [deftest is testing]] [eacl.release-guard :as guard])) (def tag-context @@ -202,14 +201,3 @@ (guard/evaluate-tag-checks "release-sha" tagged-workflow-runs (assoc-in checks [0 :conclusion] "skipped"))))))) - -(deftest release-workflow-is-tagged-and-reuses-tested-runtime-artifacts - (let [workflow (slurp ".github/workflows/release.yml") - preflight (slurp "bin/release-preflight")] - (is (string/includes? workflow "tags: ['v[0-9]*']")) - (is (not (string/includes? workflow "branches:"))) - (is (string/includes? workflow "environment: clojars")) - (is (string/includes? workflow "run-id: ${{ steps.guard.outputs.tests-run-id }}")) - (is (not (string/includes? workflow "bin/formal"))) - (is (string/includes? preflight "actions/runs?head_sha=$GITHUB_SHA&event=push")) - (is (string/includes? preflight "clojure -M:release-guard tag-checks"))))