[bootjp]

Design: docs/design/2026_09_26_partial_serializable_isolation_audit.md

Summary

Startup-lint prerequisite #1356 has merged; this PR targets main and now includes the reviewed main changes through #1367 (0b06781b2cfd5cb59e6e66d9fb0acfabe7f93c0b). This PR implements the S3 portion of A1, not the entire isolation audit. The new pushed HEAD is 1a6a6e265f2bc94fdd5c7ff66b2654f66866016d (signed, bootjp author/committer). All review/CI gates must match this SHA, not the earlier 51409d937b implementation/security checkpoint.

• Build each multipart completion from one retained read timestamp/voucher, reread all descriptors and ETags on a definitive-conflict retry, and include every consumed part descriptor in ReadKeys.
• Keep UploadPart's pre-body snapshot and immutable inline/offloaded blob namespaces. Allocate its descriptor commit timestamp after durable chunks and final state reads; validate upload, generation, and previous descriptor at exactly StartTS.
• Fence both public/admin bucket deletion by re-putting the maximum generation, without adding unrelated object writers to the bucket-meta read set.
• Preserve candidate and superseded chunks when a dispatched write may have committed. Unknown outcomes override joined conflict/lock/fence causes and cannot authorize fresh replay or destructive cleanup.
• Raise the bounded physical read-key allowance to 20,480 while preserving all existing validation and migration aliases, supporting 10,000-part completion even during staged visibility.
• Add opt-in multipart Jepsen histories alongside unchanged PUT/GET histories, mandatory successful final reads for every key, a nonvacuity gate, and unconditional encryption-specific CI history artifacts. Multipart runs 30s at rate 10/concurrency 10; no completion replay after an uncertain result.
• Security follow-up: reject public object keys above 1,024 decoded bytes before proxy/body handling and apply the same creation restriction to admin PUT. Enforce a 24 MiB logical aggregate completion read-key budget before descriptor/read-key array allocation or descriptor reads, accounting for zero escaping and fixed encoding overhead without unchecked multiplication. Admin GET/delete remain available for previously stored overlong keys. S3 object-key limit.

Regression And Validation Evidence

• Native Raft/FSM reproductions failed before the fix: completion referencing removed chunks, bucket deletion/recreation races, duplicate superseded cleanup, and default inline descriptor commit failure.
• Actual lost-success-reply reproduction failed before the fix: cleanup removed chunks referenced by the committed descriptor. Unknown-plus-conflict/lock/fence retry-chain cases also failed before the fix.
• Focused native S3 race suite passes, including both read windows, different/same-body replacement, unrelated writes, public/admin generation fencing, and 10,000 parts in normal/staged routing. Final committed-source rerun: adapter 31.913s, KV 51.694s, exit 0.
• Lost-reply retention passes for both inline/offloaded paths, including deadline-after-commit.
• KV physical capacity tests pass through actual proposal/FSM boundaries, including exact cap, pre-proposal overflow, alias conflicts, and both commit-stamping paths.
• Full local race invocation go test -p 2 -race ./adapter ./kv ./store . -count=1 -timeout=30m passed. It started before the last small candidate changes, so it is not represented as final-HEAD proof. Final committed-source focused tests and published-HEAD CI remain gates.
• Unfiltered full lint and normal commit lint hook: 0 issues. Worktree clean after the hook.
• Jepsen/CLI unit tests: 22 tests, 195 assertions, zero failures/errors, including actual loopback HTTP overlap/lost reply and fail-closed final-read cases.
• Dedicated local three-node clusters: original PUT/GET and multipart both pass with encryption off/on. One initial 5s multipart sample correctly failed with zero confirmed writes; it was not counted as acceptance. The new 30s runs pass: off has 10 confirmed writes/158 reads; on has 3 confirmed writes/162 reads. Both cover every final key with no failed final reads. Local cluster processes exited and logs/histories were preserved. These short no-nemesis runs prove these histories only, not general availability or throughput.
• Archive helper round-trip/missing-store tests and YAML parsing pass.
• Security review regression was runtime-red before correction: long ASCII/UTF-8 keys were accepted over HTTP, admin PUT accepted an overlong key, and oversized dependency sets reached descriptor loading. Post-fix native limits/max-parts/legacy recovery tests pass (34.777s); strengthened actual-proxy positive-control tests also pass (3.312s). Full unfiltered lint is 0 issues. Prior-HEAD review/CI results do not qualify the security follow-up HEAD; re-review and CI remain required.

Separate Review Passes

Main integration resolves the Jepsen workflow conflict by preserving both S3
multipart/history artifacts and the added SQS Standard workload. No workload,
timeout, iteration count, rate, concurrency or drain budget was removed/reduced.
Two unused shell bindings in that workflow were removed/renamed without changing
the 90-attempt startup loop. Actionlint passes for the changed per-push and
main-integrated scheduled workflows; archive round-trip/missing-store checks
also pass. A broader actionlint invocation still reports preexisting custom
runner-label/quoting diagnostics in the separate unchanged jepsen.yml, not a
claimed repository-wide workflow-lint success.

Post-integration S3/SQS/FIFO adapter race selection passes57.158s. The known
large-value TestMigrationQuorumPartitionAcceptance is NOT in that name selection;
it was separately run unchanged under race and passes25.046s. Full Go lint is
zero issues. The earlier two CI failures at 51409d9 remain failed artifacts:
leadership loss/outcome-unknown instead of a deterministic size rejection is not
classified as an abort or called fixed by a local pass. Fresh current-head CI
and explicit normal/security review remain mandatory before any ready/merge.

1. Data loss: immutable chunk namespaces survive commit allocation; uncertain dispatch never authorizes deleting possibly referenced blobs. Native postcommit-lost-reply tests inspect stored descriptors and chunks. Conservative retention can leave orphans rather than lose committed data.
2. Concurrency / distributed failures: coherent StartTS/voucher/pin, real apply-time dependency checks, clean retry snapshots, and generation fences cover race windows. A2 read locks remain required for full cross-group serializability.
3. Performance: completion reads O(parts); no global parts fence or unrelated bucket-writer dependency. Before the byte-budget follow-up, the metadata-only benchmark at 10,000 descriptors measured approximately 4.34–4.57ms and 4.735MB/50,040 allocations on this machine; this is not final-HEAD payload throughput or a before/after speedup claim. The dependency-byte budget is not a bound on total heap, encoding copies, or concurrency.
4. Data consistency: every consumed descriptor is validated; legacy metadata encoding remains readable; malformed-descriptor fallback is unchanged while operational read errors propagate. All changed helper callers and error retry consumers were audited.
5. Coverage: native HTTP/Raft tests, exact timestamp/read-set assertions, physical migration capacity, both storage modes, bounded actual HTTP workers, and CI encrypted off/on histories. Metadata-only maximum-part fixtures prove capacity, not 50GiB payload integrity; smaller native payload tests inspect actual bytes.

Independent Go Standards/Spec reviews had no remaining findings. Jepsen Standards review had no findings; Spec review found missing successful-history retention, now corrected and re-reviewed. Published-HEAD review and CI are required before merge.

Current-Head Acceptance

For 1a6a6e265f2bc94fdd5c7ff66b2654f66866016d, the explicit post-push
normal review completed without major findings and the independent security
review reported no security issues. The earlier advisory's original commit
is a46fba9767350874210931ad372a8a3a98d49469; its relocated inline commit
field is not a new finding against this HEAD.

• Full Go CI run 40990007218 passed, including the unchanged full-length
  gRPC consistency sequences and native quorum regression. This successful
  run does not establish a root cause or repair for the two previous failures.
• Jepsen run 40990007206 passed both encryption modes. Downloaded artifacts
  s3-acceptance-encryption-off and s3-acceptance-encryption-on independently
  identify this exact source SHA and both S3 step outcomes as success.
  The original register histories have valid? true and no failures. The
  multipart histories have valid? true, no linearizability failures, and
  respectively 7/3 confirmed writes and 166/181 successful reads. All final
  keys are present; both missing-final-key and bad-final-read lists are empty.
• An independent post-main-integration native race check covers staged and
  ordinary routing, inline and offloaded parts, concurrent replacement,
  operational read failures, legacy version-zero metadata and lost successful
  replies joined with conflicts. It passed (3.618s) without shared source edits.
• Full post-integration KV race passed (95.631s), the focused S3/SQS/FIFO
  adapter race passed (57.158s), and the unchanged native quorum test passed
  separately (25.046s). These local passes do not replace published-head CI.

All current-head CI checks, including CodeQL, have now passed. Draft was
marked ready only after those gates passed. The ready-triggered normal and
security reviews completed at 02:27:34Z and 02:29:18Z on the same HEAD;
there are no new root inline findings. The earlier explicit post-push manual
normal/security receipts remain exact-head matches. No code changes or force
push are implied by recording these receipts.

Remaining Scope

This does not close A0/A0b/A2/A6 or the full design-doc goal. In particular, #1355 has a separately reproduced P1 involving a mixed local/replicated watermark and is not a dependency to merge blindly. No deployment or production cluster changes are included.

Author: bootjp

[coderabbitai]

Caution

Review failed

The pull request is closed.

Walkthrough

S3マルチパート処理のトランザクション読み取り依存関係とキー制限を変更しました。ReadKeysの容量を拡張し、結果不明時の再試行とチャンクのクリーンアップ条件を調整しました。オプトインのJepsen multipartワークロード、回帰テスト、CI履歴アーカイブも追加しています。

Changes: S3マルチパート整合性と検証

Layer / File(s)	Summary
ReadKeys容量と物理キー上限 kv/coordinator.go, kv/read_keys_capacity_test.go, docs/design/2026_09_26_partial_serializable_isolation_audit.md	ReadKeys上限を20,480件に変更しました。ステージド可視性の物理キー展開、境界値、複数シャードの処理をテストします。
キー制限とバケット世代 adapter/s3.go, adapter/s3_admin.go, adapter/s3_admin_objects.go, adapter/s3_bucket_delete.go, adapter/s3_multipart_limits.go, adapter/s3_multipart_limits_test.go, adapter/s3_multipart_read_set_test.go, adapter/s3_multipart_occ_repro_test.go, docs/design/2026_09_26_partial_serializable_isolation_audit.md	S3オブジェクトキーの1,024バイト制限とマルチパート読み取りキーの24 MiB予算を追加しました。通常・管理者のバケット削除では、メタデータ削除と世代キーの書き込みを行います。
UploadPartのコミットと結果不明時の処理 adapter/s3.go, adapter/s3_upload_part.go, adapter/s3_hlc_fence_test.go, adapter/s3_mutation_outcome_test.go, adapter/s3_multipart_read_set_test.go, adapter/s3_multipart_occ_repro_test.go, docs/design/2026_09_26_partial_serializable_isolation_audit.md	UploadPartのReadKeysにバケット世代とパートキーを含めました。結果不明のエラーは再試行せず、コミット結果に応じてチャンクのクリーンアップを制御します。
マルチパート完了とパート読み取り依存 adapter/s3.go, adapter/s3_multipart_complete.go, adapter/s3_multipart_benchmark_test.go, adapter/s3_multipart_read_set_test.go, adapter/s3_multipart_occ_repro_test.go	完了処理は試行ごとに読み取りスナップショットを確保し、完了対象パートのキーをReadKeysに含めます。最大パート数を含むテストとベンチマークを追加しました。
JepsenマルチパートワークロードとCI jepsen/src/elastickv/s3_workload.clj, jepsen/test/elastickv/s3_workload_test.clj, .github/workflows/jepsen-test.yml, docs/design/2026_09_26_partial_serializable_isolation_audit.md	multipartワークロードはCLIで有効化します。最終読み取りcheckerとHTTP応答検証を追加し、CIで通常・multipart両方の実行履歴とメタデータを14日間保存します。

Priority: Not assessed

Estimated code review effort: 4 (Complex) | ~60 minutes

Change: Bug fix

Sequence Diagram(s)

sequenceDiagram
  participant Jepsen workload
  participant S3Server
  participant Coordinator and FSM
  participant Final-read checker
  Jepsen workload->>S3Server: multipartの開始とパートのアップロード
  S3Server->>Coordinator and FSM: パート記述子をコミット
  Jepsen workload->>S3Server: パート再アップロードと完了要求を並行実行
  S3Server->>Coordinator and FSM: 完了トランザクションを送信
  Jepsen workload->>S3Server: 全キーの最終GET
  Jepsen workload->>Final-read checker: 操作履歴を渡す

Loading

Possibly related issues

• Issue 1330 — このPRはSerializable Isolation AuditのS3マルチパート項目と検証を実装しています。監査全体の残作業を追跡するIssueの目的と関連します。

Merge Risk: Low · up to 1a6a6

The multipart changes retain data safely when write outcomes are uncertain, but some unused chunks and failed test uploads can remain until later cleanup or bucket deletion. Merge risk is low with explicit ownership of these cleanup gaps; the suggested coverage improvements strengthen validation.

Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (a46fba9):

• kv/coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (the TSO allocation floor; legacy modes have none and are pinned as known gaps), and the NextFenced ceiling fence (fail-closed when wall_now >= physicalCeiling or when the next value's physical half exceeds it). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/tso*.go — RaftTSOAllocator must Observe the committed allocation floor before reserving and commit the new floor before handing a window out (HLC.tla IssuanceMode = "tso").
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and which node stamps StartTS / CommitTS (HLC-3; legacy ShardedCoordinator stamping is the known gap G10). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on (OCC.tla; G0 / G1 are pinned as known gaps).
• kv/fsm.go, kv/fsm_migration_serving.go — FSM apply of HLC lease entries (SetPhysicalCeiling), the one-phase / PREPARE / COMMIT validation OCC.tla models, verifyComposed1, and the migration serving guard Composed.tla relies on for unpinned writes.
• store/mvcc_store.go, store/lsm_store.go — version visibility, resumable compaction, the commit-ts apply fence, and the MVCC-1 / MVCC-4 / MVCC-5 invariants.
• adapter/ts.go — the snapshot start timestamp OCC.tla assumes (applied watermark; MaxUint64 on an empty store).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-30T02:27:34.581975Z	1a6a6e2	Draft marked ready
🔒 Security Review	✅ Completed 2026-10-30T02:29:18.396283Z	1a6a6e2	Draft marked ready

Security findings

Advisory findings (1)

• 🟡 Bound multipart completion read-key bytes · Medium

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep them coming!

Reviewed commit: a46fba9767

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Here are some automated security review suggestions for this pull request.

Reviewed commit: a46fba9767

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[bootjp]

@codex review

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (51409d9):

• kv/coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (the TSO allocation floor; legacy modes have none and are pinned as known gaps), and the NextFenced ceiling fence (fail-closed when wall_now >= physicalCeiling or when the next value's physical half exceeds it). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/tso*.go — RaftTSOAllocator must Observe the committed allocation floor before reserving and commit the new floor before handing a window out (HLC.tla IssuanceMode = "tso").
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and which node stamps StartTS / CommitTS (HLC-3; legacy ShardedCoordinator stamping is the known gap G10). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on (OCC.tla; G0 / G1 are pinned as known gaps).
• kv/fsm.go, kv/fsm_migration_serving.go — FSM apply of HLC lease entries (SetPhysicalCeiling), the one-phase / PREPARE / COMMIT validation OCC.tla models, verifyComposed1, and the migration serving guard Composed.tla relies on for unpinned writes.
• store/mvcc_store.go, store/lsm_store.go — version visibility, resumable compaction, the commit-ts apply fence, and the MVCC-1 / MVCC-4 / MVCC-5 invariants.
• adapter/ts.go — the snapshot start timestamp OCC.tla assumes (applied watermark; MaxUint64 on an empty store).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Bravo.

Reviewed commit: 51409d937b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security review completed. No security issues were found in this pull request.

Reviewed commit: 51409d937b

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[bootjp]

Latest HEAD 51409d9 passed both code and security re-review. The fixed earlier security thread is resolved. Both CI S3 artifacts were downloaded and parsed as EDN, with matching run SHA and register/multipart success receipts: off multipart has valid=true, 5 confirmed writes/165 reads, no missing/bad final reads; on has valid=true, 4 confirmed writes/171 reads, no missing/bad final reads. The Go CI failed in the unchanged TestMigrationQuorumPartitionAcceptance: a 63+ MiB moving-range negative probe lost leadership and returned outcome-unknown instead of its expected deterministic size rejection. The same test passes locally 3 times under race (68.321s). This does not prove the CI failure fixed or classify unknown as an abort; the original failure is retained. The complete failed Go job was rerun on the same SHA, without reducing tests or changing assertions. Merge remains gated on its success.

[bootjp]

The complete Go rerun failed again at the same 63.5 MiB moving-range probe, returning outcome-unknown after leadership loss instead of the expected typed size rejection. This is now recurrent CI evidence, not dismissed as a one-off. Both failure logs are retained. Merge remains blocked while diagnosing large-entry transport/CPU/I/O behavior; no assertion, payload size, or quorum requirement has been weakened, and no unknown write is treated as a confirmed abort.

[bootjp]

@codex review

Please review exact new HEAD 1a6a6e2, including security review. Integrated current main 0b06781 and resolved the workflow conflict while keeping S3 multipart/history artifacts AND SQS Standard/FIFO acceptance. All workload counts/timeouts/rates/concurrency/drain settings are unchanged; two unused shell bindings were cleaned up. S3/SQS/FIFO race passes57.158s and the separately selected unchanged large-value TestMigrationQuorumPartitionAcceptance passes25.046s locally; full lint and changed-workflow actionlint/archive tests pass. Earlier 51409d native CI failures remain failed evidence, not a root-cause fix or an abort proof. Keep Draft and require all fresh CI, normal/security reviews on this exact HEAD. Check multipart read-key bounds and candidate retention against the newly integrated transaction-owner routing.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (1a6a6e2):

• kv/coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (the TSO allocation floor; legacy modes have none and are pinned as known gaps), and the NextFenced ceiling fence (fail-closed when wall_now >= physicalCeiling or when the next value's physical half exceeds it). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/tso*.go — RaftTSOAllocator must Observe the committed allocation floor before reserving and commit the new floor before handing a window out (HLC.tla IssuanceMode = "tso").
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and which node stamps StartTS / CommitTS (HLC-3; legacy ShardedCoordinator stamping is the known gap G10). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on (OCC.tla; G0 / G1 are pinned as known gaps).
• kv/fsm.go, kv/fsm_migration_serving.go — FSM apply of HLC lease entries (SetPhysicalCeiling), the one-phase / PREPARE / COMMIT validation OCC.tla models, verifyComposed1, and the migration serving guard Composed.tla relies on for unpinned writes.
• store/mvcc_store.go, store/lsm_store.go — version visibility, resumable compaction, the commit-ts apply fence, and the MVCC-1 / MVCC-4 / MVCC-5 invariants.
• adapter/ts.go — the snapshot start timestamp OCC.tla assumes (applied watermark; MaxUint64 on an empty store).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. What shall we delve into next?

Reviewed commit: 1a6a6e265f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security review completed. No security issues were found in this pull request.

Reviewed commit: 1a6a6e265f

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (1a6a6e2):

• kv/coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (the TSO allocation floor; legacy modes have none and are pinned as known gaps), and the NextFenced ceiling fence (fail-closed when wall_now >= physicalCeiling or when the next value's physical half exceeds it). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/tso*.go — RaftTSOAllocator must Observe the committed allocation floor before reserving and commit the new floor before handing a window out (HLC.tla IssuanceMode = "tso").
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and which node stamps StartTS / CommitTS (HLC-3; legacy ShardedCoordinator stamping is the known gap G10). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on (OCC.tla; G0 / G1 are pinned as known gaps).
• kv/fsm.go, kv/fsm_migration_serving.go — FSM apply of HLC lease entries (SetPhysicalCeiling), the one-phase / PREPARE / COMMIT validation OCC.tla models, verifyComposed1, and the migration serving guard Composed.tla relies on for unpinned writes.
• store/mvcc_store.go, store/lsm_store.go — version visibility, resumable compaction, the commit-ts apply fence, and the MVCC-1 / MVCC-4 / MVCC-5 invariants.
• adapter/ts.go — the snapshot start timestamp OCC.tla assumes (applied watermark; MaxUint64 on an empty store).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

Acceptance for 1a6a6e2: explicit post-push normal/security reviews passed; both ready-triggered reviews also completed at 02:27:34Z / 02:29:18Z. All current-head CI checks pass, including full Go race and unchanged full-length gRPC sequences, both Jepsen encryption modes, lint, build, CodeQL, DCO and TLA. Current-head root inline findings are empty. Downloaded S3 artifacts identify this exact SHA: both original register histories are valid; multipart histories are valid with off7/on3 confirmed writes, 166/181 successful reads, complete final keys and no bad final reads. Independent composition review found no new validated P1/P2. The old advisory originated at a46f and was corrected before this HEAD. The two earlier native quorum failures remain unproven-root-cause failures, not claimed repaired by the green run. This merges only the S3 A1 component; the full audit and async runtime remain incomplete.