Repository navigation
Conversation
Twenty-two tests never called a production namespace, or asserted something the code under test cannot change. No production code changes. - cache_strategy_adversarial_test: six tests over a model defined in the test file, for example `(= (apply max [3 1 2]) (apply max [3 1 2]))` and assertions that an inline lookup function behaves as written. The test the counterexample ledger replays stays, with the helpers it uses. - counterexamples_test: five tests that only compute on fixture data, and the in-test "mutant" evaluator. The four checks of the reference oracle stay, and the fixture keeps the four graphs they read. - experiments_test: the two self-checks of the pre-production prototype harness. The harness stays runnable from the REPL (docs/benchmarks/operator-engine.md). - characterization_fixture_test, release_test, release_guard_test, source_prep_test, module_test: six tests asserting that a workflow, script, deps file or literal set contains given text. - standard_lru_test: `storage-never-invokes-a-loader-or-validator-test` counted calls of a function the store never receives. - Datahike `current-db-reference-identity-test` described `datahike.api` only; the Datahike adapter identifies a basis by data, not by identity. - baseline_test: `baseline-invariants-test` asserted flags recorded in the saved snapshot. The same flags are now asserted on the freshly computed capture inside `frozen-baselines-reproduce-test`. Also drops one block in verified_kernel_test and one line in cache_review_regressions_test whose assertions are always true.
Sixteen tests made the same call and asserted the same result as a test that stays. Each line names the removed test and where it is still asserted. Core: - standard-lru `lookup-holds-value-across-concurrent-policy-eviction-test`: the held value was read before the eviction and nothing ran concurrently; `repeated-hot-key-survives-cold-key-churn-test`. - backend.v8 `projection-cache-free-path-has-no-cache-effects-test`: `subject->resources` never reads the subproblem store; `direct-projections-never-use-cache-owned-chunking-test`. - secure-format `source-lifecycle-is-bounded-portable-canonical-data-test`: both inputs are maps, one rejection branch; uuid-lifecycle `explicit-native-domain-test`. - secure-format `encrypted-cursors-reuse-client-private-key-context-test`: the two-cursor case of `encrypted-cursor-key-context-cache-retains-hot-context-test`. - relay `recursive-snapshot-continuation-does-not-rebase-test`: its fixture equalled the non-recursive one; `changed-proof-on-snapshot-is-a-basis-conflict-test`. Datomic: - lookup-cache `default-client-cache-has-no-ttl-test`: config-test `cursor-expiry-is-optional-and-independent-from-authorization-cache-test`. - v6-to-v7 `migrate!-rejects-unknown-options-test`: `migrate!-removed-rollback-option-is-rejected-test`, same validator with stricter assertions. - adversarial-v8-review `safe-retraction-must-not-weaken-a-caveat-into-expiry-only`, `safe-retraction-must-reject-qualifier-entity-targets` and `component-closure-must-not-delete-a-caveat-definition`: the shared safe-retraction contract run by safe-retraction `qualified-control-roles-are-protected-in-the-installed-body-test`. - cache-review-regressions `fully-consistent-reads-reuse-the-basis-pinned-exact-entry-test`: consistency-cache `can-results-obey-all-cache-consistency-modes-test`. - v8-characterization `public-api-arity-characterization-test`: the first call of the shared contract run by contract `datomic-contract-test`. DataScript: - snapshot-lifecycle `selected-snapshot-releases-when-context-construction-fails-test`: the cancellation case of `selected-snapshot-releases-across-post-selection-fault-boundaries-test`; production has one catch at that stage. - contract `raw-retraction-requires-explicit-cache-expiry-test`: `unsupported-mutation-recovery-requires-every-client-and-data-repair-test`. - continuation-reuse `default-lifecycle-is-the-portable-cross-process-constant-test`: contract `default-source-lifecycle-is-cross-client-constant-test`. - operator.recursive `public-recursive-operator-routing-can-be-disabled-test`: operator.lookup `public-acyclic-operator-routing-can-be-disabled-test`; one gate serves both plan kinds. Also drops a block in api-contract `recursive-traversal-limits-are-configurable-test` that repeated the assertion above it.
`snapshot-restore-validator-and-page-guard-fail-closed-test` built its oversized-page snapshot with `:value` outside the entry map, so the snapshot was rejected for its entry count and the page guard never ran. The entry is now well formed and the test asserts both sides of the guard: a 1,000-item page restores and a 1,001-item page is rejected. The entry-count rejection the old shape reached by accident has its own assertion.
These assertions read counters, keys or vars that production does not write on the path under test, so each compared nil with nil or zero with an upper bound. - raw_op_count_test: :compiled-recursive-plans, :stream-fills, :denotation-key-builds and :denotation-dependency-calcs have had no writer since the retired engines were removed, and no production path makes an :indexed-traversal-drive or -resume crossing. Plan seals now come from the request ledger, scans from :advanced-datoms, crossings from the sum of the kernel-crossing counter, and key builds from a counting key constructor with a store-bound control. The recorded :permission-path-calcs envelope is asserted. The dependency-calculation envelope is dropped with its counter. The interned-payload test now hands empty responses to the scan-response validator. - lookup_cache_test, cache_differential_test, bench/pagination_test: bind the engine's traversal observer; client calls never read the Datomic impl-level one. The keyset page fixture grows from 12 to 24 seeds so that its ceiling separates keyset pages from replay. - recursive_cache_test: the answer-hit check reads the live observer instead of :stream-fills. - speculative_admission_test: cache-stats has :exact-entries and :managed-entries, not :exact-size and :managed-size. A committed read is added as a control. - relay_test: the prepared query has no :opts; assert :expiring-cursor-input?. - indexed_test: redefine the engine's point-check entry points instead of impl.indexed/can?, which the raw lookup never calls, and drop a redefinition of get-permission-paths that had no effect. - contract_test (DataScript): compare adapter operations from backend/*backend-op-stats*; the public check path never writes engine/*backend-work-stats*. Drop the check for a statistics key that nothing emits. - inspection_test: also run with the counting evaluator, which :evaluator nil had replaced.
shared-tier-keeps-the-longer-prefix-under-concurrent-extension-test called the bounded store's put-if-absent! and replace-if! directly and never reached scan-cache/shared-deposit!. Its replacement runs two requests through caching-fetch-fn, the second completing inside the first one's adapter command, for an extension and for a first deposit, in both orders. It asserts exact replies, one request's prefix in the tier, no overwrite of a longer prefix by a stale shorter one, and an exact answer for a later request at the cost of at most one more command. The tier keeps the first of two racing deposits rather than the longer one, so the test accepts either where the shorter lands first.
- Sixteen nil checks of [:page-info :cursor-recovery]. No production code writes the key, and trusted_surface_audit_test pins its absence from the relay, engine and Datomic sources. - consistency_test: adapter reads counted around selected-basis-token, which takes no adapter. - stable_reducer_test: equality of a field of an immutable local map. - cache_test: one assertion made twice in a row. - standard_lru_test: a counter incremented by the test itself. - Eight (is true) placeholders in ClojureScript branches. Five tests with JVM-only bodies are now defined on the JVM only.
:closing-evidence is free text, and only the regression-vars map in the replay test is enforced, so 39 evidence strings in 28 entries had come to name tests that no longer exist: tests renamed or removed with the legacy engine and shadow mode (d96bc4c), with the analysis router (3395d96), with cursor recovery (7a3cd3e), and four names that were never committed. - A renamed test gets its current name. - A removed test is dropped. A Historical comment names it and the commit that removed it, as EACL-FORMAL-050 already does, and the entry lists its enforced regression var. - A name that never existed is replaced by the test that was meant, or dropped where none was. The same field held thirteen other dead references, fixed the same way: ten to formal/verification/*.edn ledgers removed in 483911d, one mutation id that left the registry in 2ebf743, and two Dafny lemma names in EACL-FORMAL-064 that were never real. EACL-FORMAL-004 names the lemmas TemporalSafety.dfy has now instead of its removed recovery-mode ones, and EACL-FORMAL-063 lists one test once instead of twice.
The notes described :cache-attempt with :evaluation-reserve-ms and :maximum-atomic-attempts. Those controls existed from 7a3cd3e to e25f835 and are in no tagged version: make-client rejects the key with :eacl/invalid-config and a request that carries it is rejected as an unknown key. Cache capacity is entry counts under :cache.
These tests cannot detect a defect in EACL. Each one asserts that a removed name is still absent, or restates the text of a file. - raw-db-entry-points-are-removed-test (Datahike, DataScript): two ns-resolve calls return nil. - derived-expression-metrics-are-not-schema-attributes-test (Datahike, DataScript, Datalevin) and the two Datomic schema-does-not-include tests: a schema constant holds no retired attribute. - retired-dafny-surface-is-absent-test: seven retired markers appear in no source file. The helpers only it used go with it. - no-homegrown-policy-state-is-exposed-test: three keys are nil, and a key-set check that the test above it makes by comparing the whole map. - durable-cache-contracts-forbid-request-joining-test: three spec files lack five phrases. The probe only it called goes with it. - standard-cache-source-dependencies-are-pinned: four deps.edn files equal literals. Six assertions of the same kind are dropped from tests that stay: an ns-resolve of `snapshot` in four tests, and two schema-constant checks in clean-v8-schema-retires-flat-permission-attributes-test.
Seven tests that only searched for names or text, or ran a model defined in their own file, were the enforced regression of thirteen counterexample entries. They are deleted, and each entry now names a test that executes what replaced its defective path: - 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 and validation runs once, at publication. - 037: the Datomic client's decision kernel is the generated authority. - 059: the JVM smoke test that reads the shared cross-runtime page vector. Entries 028, 031, 034, 048 and 058 record defects in CI scripts and test harnesses. Nothing in the product replays them, so the replay test gains a `tooling-defects` set: the corpus check requires every entry to be in that set or in `regression-vars`, never both, and each of those entries names the gate that failed. Deleted: deleted-trusted-surfaces-stay-deleted-test, indexed-facade-has-no-shared-schema-cache-surface-test, the two workflow text tests in characterization_fixture_test, the two text tests in the replay test, and the in-test cache model in cache_strategy_adversarial_test, with their namespaces removed from the runner lists. Every dropped name stays in its entry as a Historical comment.
2026-10-04-delete-tautological-tests modifies the two requirements that asked for the deleted tests: negative source assertions for deleted paths, and what counts as a retained counterexample regression.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Deletes 18 tests that cannot detect a defect in EACL, and 6 assertions of the same kind inside tests that stay. No production code changes.
Stacked on #230, #231 and #232. This branch contains those three, so until they merge this diff shows them too. Merge them first, or merge this one alone to take all four. The commits that belong to this PR are the last three.
What counts as tautological
A test is deleted when every assertion in it is one of these:
None of these runs the behaviour it is named after. The first can only fail if someone re-adds the name; the second fails whenever the file is edited; the third fails only if the test is edited.
Deleted
eacl.datomic.trusted-surface-audit-test/deleted-trusted-surfaces-stay-deleted-test(file removed)eacl.datomic.impl.indexed-test/indexed-facade-has-no-shared-schema-cache-surface-testns-resolvecalls return nilraw-db-entry-points-are-removed-test(Datahike, DataScript)ns-resolvecalls return nilderived-expression-metrics-are-not-schema-attributes-test(Datahike, DataScript, Datalevin)eacl.datomic.schema-test:schema-does-not-include-persisted-grants-test,schema-does-not-include-derived-expression-metrics-testeacl.formal.dafny-cleanup-gate-test/retired-dafny-surface-is-absent-testeacl.subproblem-maintenance-test/no-homegrown-policy-state-is-exposed-testeacl.characterization-fixture-test:formal-cljs-smoke-preserves-persistent-nrepl-executors-test,formal-ci-isolates-and-stops-performance-nrepls-testformal.ymland the smoke launchereacl.formal.counterexample-replay-test:replay-entrypoint-does-not-eagerly-load-formal-only-oracles-test,clean-generated-javascript-contract-expectations-testbin/formaland two smoke test sourceseacl.performance.correctness-gate-test/durable-cache-contracts-forbid-request-joining-testeacl.build.config-test/standard-cache-source-dependencies-are-pinneddeps.ednfiles equal literalseacl.formal.cache-strategy-adversarial-test/publication-and-independent-computation-traces-exhaustive-test(file removed)Six assertions of the first kind are dropped from tests that stay:
(nil? (ns-resolve … 'snapshot))in four tests, and two schema-constant checks inclean-v8-schema-retires-flat-permission-attributes-test.Ledger
Seven of the deleted tests were the enforced regression for 13 ledger entries. Each entry now points at a test that runs what replaced the defective path, or is recorded as a tooling defect.
eacl.datomic.lookup-cache-test/cache-config-is-validated-test: a caller-supplied cache provider is rejected at constructioneacl.cache.standard-lru-test/concurrent-publication-computes-independently-and-never-overwrites-testeacl.subproblem-cache-test/publication-validation-runs-once-and-never-on-hit-testeacl.datomic.api-contract-test/generated-authority-is-the-only-production-engine-testeacl.formal.production-kernel-test/generated-java-drives-production-recursive-pages, which reads the shared cross-runtime vectorThe last five record defects in CI scripts and test harnesses, not in EACL. Their "regressions" replayed a text search. The replay test gains a
tooling-defectsset, and the corpus check now requires every entry to be in that set or inregression-vars, never both. Each of those entries names the gate that failed as its closing evidence.Entries 015 and 018 only listed the audit as secondary evidence; it is dropped there. Every dropped name stays in its entry as a
;; Historical:comment.This is the part to look at. The ledger changes are in their own commit, so it can be dropped without losing the rest.
Specs
Two requirements asked for these tests, so the PR carries an OpenSpec change,
2026-10-04-delete-tautological-tests:implementation-simplicity-and-performance: "Deleted paths MUST have negative source assertions" becomes the opposite. A deleted path is not pinned by an absence or text test; what replaced it is asserted through the public API.formally-verified-authorization-engine: a retained regression must execute the code that carried the defect or the behaviour that replaced it. Two scenarios say how an entry is closed when the path was deleted and when the defect was in tooling.No pending change touches either requirement.
Left in place
These run no production code either, but they can fail for a reason, so they are not tautological:
oracle_test,counterexamples_test,generators_test,paired_test,evidence_test,mutation_control_test, the explorer latency gate).descending-merge-retains-maximum-eid-testandgeneric-merge-retains-nil-key-test(entries 019 and 020). They testeacl.lazy-merge-sort, which is no longer production code but is still what the formal smoke tests compare against the Dafny merge. Say the word if you want those two entries moved as well.formal/tree, apart from two namespace lists that named a deleted file.Verification
All run locally on this branch, one 2 GB JVM at a time.
test.ymlcommand)formal.ymleacl.datalevin.expression-storage-test(not in CI)orchestration.cljc:2656, which is(defrecord Runtime []). The audit test calledcontains?on that record with an absent key; nothing else reaches that generated accessor. No line of EACL logic lost a covered instruction or branch.tooling-defects.requireis left unused by the deletions.Not run locally: the full Dafny verification, the TLA+ jobs, the isolated-module jobs, and the rest of the Datalevin suite.
After merge, archiving the OpenSpec change folds the two requirements into the main specs.