|
77 | 77 | (is (not (:valid? result)) (str "expected mismatch, got: " result)))) |
78 | 78 |
|
79 | 79 | (deftest single-ok-concurrent-zincrby-still-validates-scores |
80 | | - ;; Codex P1: :unknown-score? must NOT be set when exactly one |
81 | | - ;; concurrent ZINCRBY is :ok (and therefore has a known resulting |
82 | | - ;; score). The read may observe either the pre-op score or the |
83 | | - ;; post-op score, both of which are in :scores. An arbitrary |
84 | | - ;; impossible score (e.g. 999.0) must still be flagged as a |
85 | | - ;; :score-mismatch, not waved through by `:unknown-score?`. |
| 80 | + ;; :unknown-score? must NOT be set when exactly one concurrent |
| 81 | + ;; ZINCRBY is :ok (and therefore has a known resulting score). The |
| 82 | + ;; read may observe either the pre-op score or the post-op score, |
| 83 | + ;; both of which are in :scores. An arbitrary impossible score |
| 84 | + ;; (e.g. 999.0) must still be flagged as a :score-mismatch, not |
| 85 | + ;; waved through by `:unknown-score?`. |
86 | 86 | (let [history [{:type :invoke :process 0 :f :zadd :value ["m1" 1] :index 0} |
87 | 87 | {:type :ok :process 0 :f :zadd :value ["m1" 1] :index 1} |
88 | 88 | {:type :invoke :process 1 :f :zincrby :value ["m1" 5] :index 2} |
|
130 | 130 | (is (:valid? result) (str "expected valid, got: " result)))) |
131 | 131 |
|
132 | 132 | (deftest duplicate-members-are-flagged |
133 | | - ;; CodeRabbit finding: ZRANGE must not return the same member twice. |
| 133 | + ;; ZRANGE must not return the same member twice. |
134 | 134 | ;; With a hypothetical committed + concurrent score for the same |
135 | 135 | ;; member, a duplicate could sneak past sort + score-membership |
136 | 136 | ;; checks. Enforce distinctness explicitly. |
|
143 | 143 | (is (not (:valid? result)) (str "expected duplicate-members error, got: " result)))) |
144 | 144 |
|
145 | 145 | (deftest overlapping-committed-zadds-allow-either-score |
146 | | - ;; CodeRabbit finding: two :ok ZADDs for the same member whose |
| 146 | + ;; Two :ok ZADDs for the same member whose |
147 | 147 | ;; invoke/complete windows overlap have ambiguous serialization |
148 | 148 | ;; order. Either's resulting score is a valid post-state; the checker |
149 | 149 | ;; must not pin to the higher :complete-idx value only. |
|
163 | 163 | (str "expected valid under overlapping-writes relaxation, got: " result)))) |
164 | 164 |
|
165 | 165 | (deftest info-before-read-is-considered-uncertain |
166 | | - ;; CodeRabbit finding: an :info mutation that completed before a |
| 166 | + ;; An :info mutation that completed before a |
167 | 167 | ;; later read may have taken effect. It must be considered a possible |
168 | 168 | ;; source of state for that read, rather than being ignored by both |
169 | 169 | ;; model-before and the concurrent window. |
|
183 | 183 | (str "expected :info-before-read to skip strict score check, got: " result)))) |
184 | 184 |
|
185 | 185 | ;; --------------------------------------------------------------------------- |
186 | | -;; Stale-read / phantom / superseded-committed checks (gemini HIGH) |
| 186 | +;; Stale-read / phantom / superseded-committed checks |
187 | 187 | ;; --------------------------------------------------------------------------- |
188 | 188 |
|
189 | 189 | (deftest phantom-member-is-flagged |
190 | | - ;; gemini HIGH: a read that observes a member which was never added |
| 190 | + ;; A read that observes a member which was never added |
191 | 191 | ;; (no ZADD/ZINCRBY/true-ZREM anywhere) must be rejected. |
192 | 192 | (let [history [{:type :invoke :process 0 :f :zrange-all :index 0} |
193 | 193 | {:type :ok :process 0 :f :zrange-all |
|
199 | 199 | (str "expected :unexpected-presence, got kinds=" kinds)))) |
200 | 200 |
|
201 | 201 | (deftest phantom-from-info-zrem-still-flagged |
202 | | - ;; gemini HIGH (round 2): an :info ZREM is the ONLY history contact |
| 202 | + ;; An :info ZREM is the ONLY history contact |
203 | 203 | ;; with a member (no ZADD/ZINCRBY ever). Because completed-mutation- |
204 | 204 | ;; window defaults :removed? to true on :info ZREMs (for uncertainty |
205 | 205 | ;; accounting), the checker must NOT treat ZREM as proof the member |
|
224 | 224 | (str "expected :unexpected-presence, got kinds=" kinds)))) |
225 | 225 |
|
226 | 226 | (deftest stale-read-after-committed-zrem-is-flagged |
227 | | - ;; gemini HIGH: once a ZADD and a subsequent real (:removed? true) ZREM |
| 227 | + ;; Once a ZADD and a subsequent real (:removed? true) ZREM |
228 | 228 | ;; have BOTH committed (with no concurrent re-add), a later read that |
229 | 229 | ;; still sees the member must be rejected as a stale read. |
230 | 230 | (let [history [;; Add then remove m1 — both committed before any read. |
|
243 | 243 | (str "expected :unexpected-presence, got kinds=" kinds)))) |
244 | 244 |
|
245 | 245 | (deftest superseded-committed-score-is-not-allowed |
246 | | - ;; gemini HIGH: a ZADD committed BEFORE another ZADD for the same |
| 246 | + ;; A ZADD committed BEFORE another ZADD for the same |
247 | 247 | ;; member whose invoke strictly followed it should not be treated as |
248 | 248 | ;; a valid post-state score. Only the latest committed score (plus |
249 | 249 | ;; concurrent in-flight) may be observed. |
|
267 | 267 | ;; --------------------------------------------------------------------------- |
268 | 268 |
|
269 | 269 | ;; --------------------------------------------------------------------------- |
270 | | -;; Linearization of concurrent ops / uncertain mutations (gemini HIGH batch 2) |
| 270 | +;; Linearization of concurrent ops / uncertain mutations |
271 | 271 | ;; --------------------------------------------------------------------------- |
272 | 272 |
|
273 | 273 | (deftest concurrent-zadd-zrem-both-completed-accepts-either-outcome |
274 | | - ;; gemini HIGH: ZADD and ZREM for the same member whose invoke/complete |
| 274 | + ;; ZADD and ZREM for the same member whose invoke/complete |
275 | 275 | ;; windows overlap (both commit before the read) have ambiguous |
276 | 276 | ;; linearization. A linearizable store may serialize either one last, |
277 | 277 | ;; so the read legitimately observes EITHER [["m1" 1.0]] OR []. |
|
294 | 294 | "expected read observing ZREM's outcome (absent) to be accepted"))) |
295 | 295 |
|
296 | 296 | (deftest info-zrem-concurrent-with-read-allows-missing-member |
297 | | - ;; gemini HIGH: an :info ZREM that might have applied before a read |
| 297 | + ;; An :info ZREM that might have applied before a read |
298 | 298 | ;; leaves the member's presence uncertain. A ZRANGE that omits the |
299 | 299 | ;; member must NOT be flagged as a completeness failure. |
300 | 300 | (let [history [;; ZADD m1 committed before the read. |
|
312 | 312 | (str "expected :info ZREM to make absence acceptable, got: " result)))) |
313 | 313 |
|
314 | 314 | (deftest info-zincrby-does-not-flag-zrangebyscore-completeness |
315 | | - ;; gemini HIGH: a pre-read :info / concurrent ZINCRBY leaves the |
| 315 | + ;; A pre-read :info / concurrent ZINCRBY leaves the |
316 | 316 | ;; resulting score unknown. ZRANGEBYSCORE filtering on a specific |
317 | 317 | ;; range must not flag the member as missing, because its score may |
318 | 318 | ;; have moved outside [lo, hi]. |
|
359 | 359 | (str "expected :missing-member, got kinds=" kinds)))) |
360 | 360 |
|
361 | 361 | ;; --------------------------------------------------------------------------- |
362 | | -;; Failed-concurrent mutations must not contribute to uncertainty (codex P1) |
| 362 | +;; Failed-concurrent mutations must not contribute to uncertainty |
363 | 363 | ;; --------------------------------------------------------------------------- |
364 | 364 |
|
365 | 365 | (deftest failed-concurrent-zrem-does-not-relax-must-be-present |
366 | | - ;; codex P1: a concurrent ZREM that completes with :fail did NOT take |
| 366 | + ;; A concurrent ZREM that completes with :fail did NOT take |
367 | 367 | ;; effect. Its window must NOT make the member's presence uncertain, |
368 | 368 | ;; so a read that omits the member (which was ZADDed and committed |
369 | 369 | ;; beforehand) must be flagged as :missing-member. |
|
386 | 386 | (str "expected :missing-member, got kinds=" kinds)))) |
387 | 387 |
|
388 | 388 | (deftest failed-concurrent-zadd-does-not-contribute-allowed-score |
389 | | - ;; codex P1: a concurrent ZADD that completes with :fail did NOT take |
| 389 | + ;; A concurrent ZADD that completes with :fail did NOT take |
390 | 390 | ;; effect. Its score must NOT be added to the allowed set. A read |
391 | 391 | ;; observing that score must be flagged as :score-mismatch rather than |
392 | 392 | ;; being waved through by the failed ZADD's ghost contribution. |
|
410 | 410 |
|
411 | 411 | ;; --------------------------------------------------------------------------- |
412 | 412 | ;; Chained committed ZINCRBYs: only the linearization-chain tail is a |
413 | | -;; valid final score. Earlier intermediate return values are stale. (codex P1) |
| 413 | +;; valid final score. Earlier intermediate return values are stale. |
414 | 414 | ;; --------------------------------------------------------------------------- |
415 | 415 |
|
416 | 416 | (deftest chained-committed-zincrby-rejects-stale-intermediate |
417 | | - ;; codex P1: sequential committed ZINCRBYs form a forced linearization |
| 417 | + ;; Sequential committed ZINCRBYs form a forced linearization |
418 | 418 | ;; chain. The first ZINCRBY's return value is an intermediate that no |
419 | 419 | ;; post-chain read may observe. Expect :score-mismatch on the stale |
420 | 420 | ;; intermediate. |
|
442 | 442 | (str "expected :score-mismatch, got kinds=" kinds)))) |
443 | 443 |
|
444 | 444 | (deftest chained-committed-zincrby-accepts-latest |
445 | | - ;; codex P1: same history but the read observes the LATEST chain tail |
| 445 | + ;; Same history but the read observes the LATEST chain tail |
446 | 446 | ;; (6.0) -- accept as valid. |
447 | 447 | (let [history [{:type :invoke :process 0 :f :zadd :value ["m1" 1] :index 0} |
448 | 448 | {:type :ok :process 0 :f :zadd :value ["m1" 1] :index 1} |
|
458 | 458 | (str "expected chain-tail score to be accepted, got: " result)))) |
459 | 459 |
|
460 | 460 | (deftest concurrent-zincrby-both-admissible |
461 | | - ;; codex P1: two overlapping-in-real-time ZINCRBYs whose returned |
| 461 | + ;; Two overlapping-in-real-time ZINCRBYs whose returned |
462 | 462 | ;; scores are BOTH candidate final states under some linearization. |
463 | 463 | ;; Read observing either value must be accepted. |
464 | 464 | ;; Overlap: A=[inv=2, cmp=5], B=[inv=3, cmp=4]. |
|
484 | 484 | "expected A's return value (6.0) admissible under overlap"))) |
485 | 485 |
|
486 | 486 | (deftest zadd-resets-zincrby-chain |
487 | | - ;; codex P1: a committed ZADD between ZINCRBYs resets the chain -- |
| 487 | + ;; A committed ZADD between ZINCRBYs resets the chain -- |
488 | 488 | ;; subsequent ZINCRBYs operate on the new ZADD'd value. The pre-reset |
489 | 489 | ;; ZINCRBY score is NOT a valid read after the chain completes. |
490 | 490 | (let [base [;; ZADD m1 1 |
|
517 | 517 | ;; :ok ZINCRBYs with known return values do NOT make the score check |
518 | 518 | ;; unknown -- their return values pin the linearization and the |
519 | 519 | ;; admissible score set is constrained by :scores (candidates + uncertain |
520 | | -;; ok return values). (codex P1) |
| 520 | +;; ok return values). |
521 | 521 | ;; --------------------------------------------------------------------------- |
522 | 522 |
|
523 | 523 | (deftest two-ok-concurrent-zincrbys-reject-impossible-score |
524 | | - ;; codex P1: two overlapping :ok ZINCRBYs with known return values |
| 524 | + ;; Two overlapping :ok ZINCRBYs with known return values |
525 | 525 | ;; (3 and 6) constrain the admissible post-chain read set to {1,3,6}. |
526 | 526 | ;; A read of 999 is impossible under any linearization; the checker |
527 | 527 | ;; must flag it as :score-mismatch (no longer swallowed by the old |
|
545 | 545 | (str "expected :score-mismatch, got kinds=" kinds)))) |
546 | 546 |
|
547 | 547 | (deftest two-ok-concurrent-zincrbys-accept-known-chain-tail |
548 | | - ;; codex P1: same concurrent :ok ZINCRBY history, but the read |
| 548 | + ;; Same concurrent :ok ZINCRBY history, but the read |
549 | 549 | ;; observes one of the recorded return values. Both 3.0 (linearization |
550 | 550 | ;; where +3 ran first, then +2) and 6.0 (the other order) must be |
551 | 551 | ;; accepted as valid. |
|
569 | 569 | "expected 3.0 (other linearization) to be accepted"))) |
570 | 570 |
|
571 | 571 | (deftest info-plus-ok-concurrent-zincrby-stays-unknown |
572 | | - ;; codex P1: when at least one concurrent ZINCRBY is :info (unknown |
| 572 | + ;; When at least one concurrent ZINCRBY is :info (unknown |
573 | 573 | ;; post-op score), the strict score check must be relaxed regardless |
574 | 574 | ;; of how many other :ok ZINCRBYs are concurrent. Any numeric score |
575 | 575 | ;; must be accepted for this read. |
|
596 | 596 | ;; --------------------------------------------------------------------------- |
597 | 597 |
|
598 | 598 | ;; --------------------------------------------------------------------------- |
599 | | -;; Client setup! / invoke! robustness (gemini MEDIUM) |
| 599 | +;; Client setup! / invoke! robustness |
600 | 600 | ;; --------------------------------------------------------------------------- |
601 | 601 |
|
602 | 602 | (deftest setup-bang-hard-fails-when-conn-spec-missing |
603 | | - ;; gemini HIGH: if open! failed to populate :conn-spec (unresolvable |
| 603 | + ;; If open! failed to populate :conn-spec (unresolvable |
604 | 604 | ;; host, etc.), setup! MUST throw rather than silently proceed. |
605 | 605 | ;; Continuing with a no-op setup would leave stale data from a prior |
606 | 606 | ;; run under zset-key and risk false-positive checker verdicts from |
|
612 | 612 | "setup! must throw ex-info when :conn-spec is nil"))) |
613 | 613 |
|
614 | 614 | (deftest setup-bang-hard-fails-when-cleanup-del-errors |
615 | | - ;; gemini MEDIUM: even when :conn-spec is populated, if the actual |
| 615 | + ;; Even when :conn-spec is populated, if the actual |
616 | 616 | ;; cleanup (DEL zset-key) fails or errors, setup! must NOT silently |
617 | 617 | ;; proceed. Stale data surviving from a prior run under zset-key |
618 | 618 | ;; would cause false-positive safety verdicts. Propagate the |
|
626 | 626 | "setup! must propagate cleanup failures, not swallow them"))) |
627 | 627 |
|
628 | 628 | (deftest zincrby-invoke-handles-nil-response |
629 | | - ;; gemini MEDIUM: if car/wcar for ZINCRBY returns nil (error reply |
| 629 | + ;; If car/wcar for ZINCRBY returns nil (error reply |
630 | 630 | ;; coerced, unexpected protocol edge), the op must complete as :info |
631 | 631 | ;; with a structured :error, not throw NumberFormatException from |
632 | 632 | ;; parse-double-safe swallowing (str nil) -> "nil". |
|
642 | 642 | (str "expected :error to be populated, got: " result)))))) |
643 | 643 |
|
644 | 644 | (deftest zincrby-invoke-handles-unexpected-response |
645 | | - ;; gemini MEDIUM: same guard, but for a non-string / non-number reply. |
| 645 | + ;; Same guard, but for a non-string / non-number reply. |
646 | 646 | ;; Must complete :info rather than propagate a parse failure. |
647 | 647 | (let [client (workload/->ElastickvRedisZSetSafetyClient |
648 | 648 | {} {:pool {} :spec {:host "localhost" :port 6379 |
|
667 | 667 | (is (= ["m1" 7.0] (:value result))))))) |
668 | 668 |
|
669 | 669 | ;; --------------------------------------------------------------------------- |
670 | | -;; Vacuous-pass guard (codex P1) |
| 670 | +;; Vacuous-pass guard |
671 | 671 | ;; --------------------------------------------------------------------------- |
672 | 672 |
|
673 | 673 | (deftest empty-history-is-unknown-not-valid |
674 | | - ;; codex P1: an empty history (e.g. Redis unreachable, all ops |
| 674 | + ;; An empty history (e.g. Redis unreachable, all ops |
675 | 675 | ;; downgraded to :info) produces zero successful reads. The checker |
676 | 676 | ;; MUST NOT return :valid? true in that case -- that would be a |
677 | 677 | ;; false-green. Expect :valid? :unknown plus a diagnostic :reason. |
|
683 | 683 | (is (zero? (:reads result))))) |
684 | 684 |
|
685 | 685 | (deftest all-info-history-is-unknown-not-valid |
686 | | - ;; codex P1: a run where every operation was downgraded to :info |
| 686 | + ;; A run where every operation was downgraded to :info |
687 | 687 | ;; (Redis unreachable / every read timed out) still has read-pairs |
688 | 688 | ;; filtered down to zero :ok reads. Must surface as :valid? :unknown. |
689 | 689 | (let [history [{:type :invoke :process 0 :f :zadd :value ["m1" 1] :index 0} |
|
708 | 708 | (str "expected :valid? true with one :ok read, got: " result)))) |
709 | 709 |
|
710 | 710 | (deftest zrem-invoke-handles-nil-response |
711 | | - ;; gemini MEDIUM: if car/wcar for ZREM returns nil (protocol edge, |
| 711 | + ;; If car/wcar for ZREM returns nil (protocol edge, |
712 | 712 | ;; closed connection, etc.), `(long nil)` would throw NPE and the |
713 | 713 | ;; op would be logged as a generic failure via the general Exception |
714 | 714 | ;; handler. Guard with `(or removed 0)` so the op resolves cleanly |
|
736 | 736 | (is (= ["m1" true] (:value result))))))) |
737 | 737 |
|
738 | 738 | (deftest parse-withscores-handles-inf-strings |
739 | | - ;; gemini HIGH: Redis returns "inf" / "+inf" / "-inf" for infinite |
| 739 | + ;; Redis returns "inf" / "+inf" / "-inf" for infinite |
740 | 740 | ;; ZSET scores. Double/parseDouble expects "Infinity"; the workload's |
741 | 741 | ;; parser must normalize both encodings instead of throwing. |
742 | 742 | (let [flat ["m-pos" "inf" |
|
0 commit comments