Delete tautological tests

.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)))

docs/benchmarks/operator-engine.md

@@ -14,7 +14,7 @@ Use a project nREPL with the `:dev:test` aliases:
 
 ```sh
 clj-nrepl-eval -p <port> "(require 'eacl.engine.physical-route-test :reload) (clojure.test/run-tests 'eacl.engine.physical-route-test)"
-clj-nrepl-eval -p <port> "(require 'eacl.operator-engine.experiments-test :reload) (clojure.test/run-tests 'eacl.operator-engine.experiments-test)"
+clj-nrepl-eval -p <port> "(require 'eacl.operator-engine.experiments :reload) (eacl.operator-engine.experiments/run-all)"
 clj-nrepl-eval -p <port> "(require 'eacl.baseline.perf :reload) (eacl.baseline.perf/capture-perf!)"
 ```
 

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

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

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}

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"]}