[bootjp]

Design: docs/design/2026_08_29_partial_tso_batch_slot_claims.md
Depends on #1364. Draft: the revised protocol is not connected to production admission.

Revised contract

Group 0 owns unique, monotonic, failover-fenced timestamp issuance. Operation-to-timestamp associations belong to the data group and must be committed atomically with the write or PREPARE. The earlier group-0 per-slot ClaimBatch design is withdrawn. A returned timestamp may be an unused gap; a successful data-group Raft apply is the durability point for its operation binding.

Current changes

• Remove the previous per-slot claim ledger, credential/snapshot protocol, and claim-aware forwarding paths from this PR.
• Retain the independently tested exact prepared-version comparison and cleanup store capability.
• Add immutable dual-index bindings in the data group: operation ID, timestamp, manifest digest, and creation phase. Exact retries skip the data apply and conflicting bindings fail.
• Add opt-in atomic FSM apply for raw, one-phase, and PREPARE creation. Production admission still rejects the new operation-ID field.
• Add local operation-ID lookup with reverse-index consistency checks for future unknown-outcome reconciliation. Absence is authoritative only after a leader read barrier.
• Add opt-in group-0 physical-band reservation. It commits the full band end and serves logical offsets locally, including safe rollover, term change, ceiling change, and ambiguous proposal tests. It has no wire route and rejects active Phase D.
• Update the design and rollout gates.

Required before activation

• Version the reservation response and wire the physical-band issuer. Old response semantics cannot describe multiple reservations from one committed band.
• Establish trusted issuance provenance at the receiving data leader; a numeric value inside a committed band is not sufficient. Reject unproven forwarded creation.
• Persist the primary/home decision before secondary PREPARE and verify the full participant manifest across groups. COMMIT/ABORT must use the bound PREPARE evidence.
• Reconcile unknown outcomes by operation ID through an authoritative leader read barrier.
• Complete retention, snapshot/restore, rolling-upgrade, whole-cluster Phase-D fencing, authentication, fault, Jepsen, and performance gates.

This branch remains Draft and does not claim the range-validation hole is closed in production.

Verification

• Full go test ./kv -count=1: pass with local listener access.
• Focused binding and physical-band tests: pass.
• golangci-lint run ./kv ./proto --timeout=5m: 0 issues.
• Signed, DCO-compliant commit verified.

Author: bootjp

Summary by CodeRabbit

• 新機能
  • 書き込みやトランザクションの作成時に、操作IDと永続化タイムスタンプの対応関係を記録し、同一内容の再試行を安全に扱えるようになりました。
  • TSOが物理時間の範囲を予約して論理スロットを割り当てる仕組みを追加しました。リーダー交代時には以前の範囲を再利用しません。
  • 準備済みトランザクションの変更を、競合を検証したうえで適用できるようになりました。
• ドキュメント
  • タイムスタンプ割り当ての設計と導入条件を更新しました。条件が整うまでは従来のプロトコルを維持します。

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 23 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: f94f2aec-5786-4af8-9d99-e37e5321eaa1

Commits

Reviewing files that changed from the base of the PR and between 1c4d687 and 76014f6.

Files ignored due to path filters: 1

• proto/internal.pb.go is excluded by !**/*.pb.go

Files selected for processing: 20

• docs/design/2026_08_29_partial_tso_batch_slot_claims.md
• kv/fsm.go
• kv/timestamp_admission.go
• kv/timestamp_binding.go
• kv/timestamp_binding_apply.go
• kv/timestamp_binding_apply_test.go
• kv/timestamp_binding_fsm_test.go
• kv/timestamp_binding_lookup.go
• kv/timestamp_binding_lookup_test.go
• kv/timestamp_binding_request.go
• kv/timestamp_binding_test.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.go
• proto/internal.proto
• store/prepared_mutations.go
• store/prepared_mutations_concurrency_test.go
• store/prepared_mutations_entry_test.go
• store/prepared_mutations_pebble.go
• store/prepared_mutations_test.go

Walkthrough

作成要求の操作IDと永続化タイムスタンプをRaft適用時に結び付ける処理を追加しました。TSO物理帯予約とprepared mutationの検証・適用も追加しました。設計文書は有効化条件と未実装の経路を記載します。

Changes: タイムスタンプ束縛と物理帯予約

Layer / File(s)	Summary
束縛プロトコルと記録形式 docs/design/2026_08_29_partial_tso_batch_slot_claims.md, proto/internal.proto, kv/timestamp_binding.go	設計文書は旧来のgroup 0 per-slot claim案に代わる方針と実装段階を記載します。Requestにoperation IDを追加し、TimestampBindingのレコード形式と双方向キーを定義します。
束縛付き作成と再試行検証 kv/fsm.go, kv/timestamp_admission.go, kv/timestamp_binding*.go	FSMは単一の束縛付き作成要求を処理し、複数要求にoperation IDが含まれる場合は拒否します。束縛と書き込みを同じRaftエントリで適用し、完全一致の再試行を重複適用せず、競合を拒否します。メモリおよびPebbleストアのテストで動作を確認します。
TSO物理帯の予約 kv/tso_raft.go, kv/tso_raft_band.go, kv/tso_raft_band_test.go	物理帯の予約、帯域内の論理スロット割り当て、termや物理上限の変更時のキャッシュ無効化を追加します。テストは曖昧な提案結果、通常予約との関係、Phase D中の拒否も確認します。

Prepared mutationの検証と適用

Layer / File(s)	Summary
期待バージョンとcleanup条件 store/prepared_mutations.go	期待バージョンとcleanupキーの条件を検証します。条件を満たすcleanup削除だけを競合判定の対象外とし、その他の変更とread keyには競合検査を適用します。
Raft適用とストア検証 store/prepared_mutations_pebble.go, store/prepared_mutations*_test.go	prepared mutationをRaftスコープ内で適用するPebble経路を追加します。テストは競合、部分適用の防止、暗号化値の読み取り整合性、適用indexを検証します。

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

Change: Feature

Sequence Diagram(s)

sequenceDiagram
  participant Request as 作成要求
  participant FSM as kvFSM
  participant Apply as ApplyTimestampBoundCreation
  participant Store as Raftエントリ内ストア
  Request->>FSM: operation ID付き要求
  FSM->>Apply: 束縛付き作成を適用
  Apply->>Store: 束縛をステージ
  Apply->>Store: 同じRaftエントリで作成処理を実行
  Store-->>Apply: 適用結果
  Apply-->>FSM: 成功またはエラー

Loading

Possibly related issues

• Issue 1330: 操作とタイムスタンプの永続的な結び付けを扱います。このPRはその基盤を追加しますが、本番経路や残りの要件は未完了とされています。

Possibly related PRs

• bootjp/elastickv#1090: PREPARE要求とロックに確定済みCommitTSを記録します。本PRはPREPARE作成時の操作IDとタイムスタンプの束縛を扱います。
• bootjp/elastickv#1355: raw適用とPREPAREをwatermarkで拒否します。本PRの再試行時の適用省略も、同じ作成経路のフェンス動作に関係します。
• bootjp/elastickv#1348: 同一タイムスタンプの衝突とMVCC書き込みを扱います。本PRはタイムスタンプと操作IDの競合を拒否する処理を追加します。

Merge Risk: Low · previous review 1c4d6

The foundation has bounded issues: an opt-in reservation can fail despite available capacity, and a timing-sensitive test can fail for correct behavior. Production admission remains disabled for binding requests, so merge risk is low with these limitations understood.

Pre-merge checks: 4 · 1

Failed checks: 1 warning

Check name	Status	Explanation	Resolution
Docstring Coverage		Docstring coverage is 12.20% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documenta…	Write docstrings for the functions missing them to satisfy the coverage threshold.

Passed checks: 4 passed

Check name	Status	Explanation
Description Check		Check skipped - CodeRabbit’s high-level summary is enabled.
Title check		タイトルは、データグループで操作とタイムスタンプを結び付ける基盤の追加を明確に示しています。
Linked Issues check		Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check		Check skipped because no linked issues were found for this pull request.

Full details: Docstring Coverage

Explanation

Docstring coverage is 12.20% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 41 functions across 18 files. (2 skipped: 2 unsupported.)

Resolution

Write docstrings for the functions missing them to satisfy the coverage threshold.

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

[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 (d142a2d):

• distribution/bootstrap_plan.go
• distribution/bootstrap_plan_test.go
• kv/coordinator.go
• kv/fsm.go
• kv/sharded_coordinator.go
• kv/tso.go
• kv/tso_claim.go
• kv/tso_claim_admission.go
• kv/tso_claim_benchmark_test.go
• kv/tso_claim_combiner.go
• kv/tso_claim_combiner_test.go
• kv/tso_claim_crash_test.go
• kv/tso_claim_decoders.go
• kv/tso_claim_fsm.go
• kv/tso_claim_fsm_test.go
• kv/tso_claim_identity.go
• kv/tso_claim_intent_fsm.go
• kv/tso_claim_issue.go
• kv/tso_claim_large_payload_test.go
• kv/tso_claim_live_benchmark_test.go
• kv/tso_claim_live_combiner.go
• kv/tso_claim_live_combiner_test.go
• kv/tso_claim_live_reopen_test.go
• kv/tso_claim_mutation_evidence.go
• kv/tso_claim_mutation_evidence_test.go
• kv/tso_claim_participants.go
• kv/tso_claim_prepared_retry_test.go
• kv/tso_claim_production_test.go
• kv/tso_claim_raft.go
• kv/tso_claim_raft_test.go
• kv/tso_claim_request.go
• kv/tso_claim_resolution_metadata_test.go
• kv/tso_claim_routing.go
• kv/tso_claim_seed.go
• kv/tso_claim_seed_darwin.go
• kv/tso_claim_seed_linux.go
• kv/tso_claim_seed_other.go
• kv/tso_claim_seed_test.go
• kv/tso_claim_seed_unix.go
• kv/tso_claim_snapshot.go
• kv/tso_claim_snapshot_test.go
• kv/tso_claim_wire.go
• kv/tso_claim_wrappers.go
• kv/tso_fsm.go
• kv/tso_raft.go
• store/lsm_store.go
• store/mvcc_store.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

Review exact latest pushed HEADd142a2d3784b1795915a5eae1f572e5ca5a32220 including security. This is a Draft TSO design checkpoint depending on #1364 (shared dependency commits; TSO-only comparison starts6346b981). Claim-aware configured Next waits group0 commit/apply; default legacy issuance and production activation/auth remain unchanged/unimplemented.
New: typed compact-v2 receiver-recomputed mutation evidence, exact owner/operation/intent/role and full participant/prefix binding, prepared-version atomic store capability, durable capsule resolution and exact prior decision reuse, explicit seed custody. Large-value full-body duplication P2 reproduced with maintained old-source RED (33MiB claim rejection;22MiB Forward69206575>67108864) then fixed without limit growth. Native single-voter TSO/data Raft+Pebble Forward/readback passes22/33/63.5MiB with sub1KiB manifests. Nine unsigned alias/bypass/unknown-meta resolution cases also reproduced RED then fixed with nil/subset resolver compatibility. User/read OCC remains originalStartTS; only exact prepared cleanup versions are exempt.
Final identical Go-source local gates: wholeKV race2319pass/fail0skip0 88.670s; final focused claim/2PC/tamper race3 27.722s, adapterrace3 13.702s; full lint0 and compile-all(no executed-test claim). Independent crypto/schema/capsule/projection review clear, small adversarial probes race3. Linuxarm64 Go1.27.2 networknone2CPU4GiB selected compact/2PC/resolution1.581s, actualnativeLargeForward4.485s. Signed bootjp/contact+DCO, remoteVerified. Require fresh latest-HEAD reviews and ALLCI; no old receipts.
Do not mark ready/merge: production authenticated registration, commit-time policy/decoder/future-member fences, unknown-attempt journal, full control/snapshot/retention/legacy-route/multinode fault/Jepsen activation/performance acceptance remain open. Partial components and native single-voter tests are not operational readiness or complete vulnerability closure.

[chatgpt-codex-connector]

Codex Review Summary: ✅ Completed

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

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-11T12:02:36.954124Z	76014f6	Manual request
🔒 Security Review	✅ Completed 2026-11-11T12:05:21.598886Z	76014f6	Manual request

Security findings

Advisory findings (2)

• 🟡 Bind transaction phase into signed claims · Medium · Resolved
• 🟡 Keep disabled binding fields deterministic across versions · 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. Nice work!

Reviewed commit: d142a2d378

ℹ️ 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: d142a2d378

ℹ️ 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 (67fc9b3):

• distribution/bootstrap_plan.go
• distribution/bootstrap_plan_test.go
• kv/coordinator.go
• kv/fsm.go
• kv/sharded_coordinator.go
• kv/tso.go
• kv/tso_claim.go
• kv/tso_claim_admission.go
• kv/tso_claim_benchmark_test.go
• kv/tso_claim_combiner.go
• kv/tso_claim_combiner_test.go
• kv/tso_claim_crash_test.go
• kv/tso_claim_decoders.go
• kv/tso_claim_fsm.go
• kv/tso_claim_fsm_test.go
• kv/tso_claim_identity.go
• kv/tso_claim_intent_fsm.go
• kv/tso_claim_issue.go
• kv/tso_claim_large_payload_test.go
• kv/tso_claim_live_benchmark_test.go
• kv/tso_claim_live_combiner.go
• kv/tso_claim_live_combiner_test.go
• kv/tso_claim_live_reopen_test.go
• kv/tso_claim_mode.go
• kv/tso_claim_mode_test.go
• kv/tso_claim_mutation_evidence.go
• kv/tso_claim_mutation_evidence_test.go
• kv/tso_claim_participants.go
• kv/tso_claim_prepared_retry_test.go
• kv/tso_claim_production_test.go
• kv/tso_claim_raft.go
• kv/tso_claim_raft_test.go
• kv/tso_claim_request.go
• kv/tso_claim_resolution_metadata_test.go
• kv/tso_claim_routing.go
• kv/tso_claim_seed.go
• kv/tso_claim_seed_darwin.go
• kv/tso_claim_seed_linux.go
• kv/tso_claim_seed_other.go
• kv/tso_claim_seed_test.go
• kv/tso_claim_seed_unix.go
• kv/tso_claim_snapshot.go
• kv/tso_claim_snapshot_test.go
• kv/tso_claim_wire.go
• kv/tso_claim_wrappers.go
• kv/tso_fsm.go
• kv/tso_raft.go
• store/lsm_store.go
• store/mvcc_store.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

Please review exact latest pushed HEAD 67fc9b37d08424f52be8414f90264b7e54dc4d8c, including security.

Fixed the phase-substitution security finding from d142 (root4421887333).
Protocol v3 signs IsTxn plus InitialPhase; raw/1PC/PREPARE cannot substitute
for one another, and irrelevant or dual PrepareCommitTS/CommitTS slots fail.
COMMIT/ABORT retain the original signed PREPARE manifest and require its exact
durable capsule. Sharded participants must share the creation phase.

The identical maintained actual Forward/Raft regression on d142 accepted the
forged 1PC and published unprepared data (RED1.912s). On this correction,
mode/signature/metadata controls pass race3 (KV1.778s), and actual PREPARE,
COMMIT/ABORT plus idempotent replay pass race3 (adapter4.294s). Final wholeKV
race: 2343pass/0fail/0skip87.984s; full lint0, including commit hook.
Independent read-only delta and final-predicate review found no P1/P2.
Linux-arm64 Go1.27.2 networknone2CPU4GiB selected mode/2PC/retry KV1.699s,
actual mode/resolve/native22/33/63.5MiB adapter4.947s. Final Go source is
byte-identical to that isolated tested export.

Also fixed Proto CI by regenerating through pinned Buf instead of standalone
protoc; all generated outputs independently reproduced byte-for-byte.
The Go CI failed one actual native leadership-transfer test at its original
60-second context. The three heavy native adapter fixtures now run in their own
race phase without other packages' competition. Full test union, payloads,
assertions and internal deadlines remain unchanged; full-length gRPC remains
last. Native fixtures pass race3 locally117.033s; no OOM root-cause claim.
All timestamp-claim adapter/native acceptance selected cases pass40.542s.

Please use only fresh receipts for this HEAD. CI is rerunning; old d142 review
and CI results are stale. This remains a Draft partial design checkpoint:
authenticated registry/commit-time authority, all-member/future-member fences,
unknown-attempt ingress journal, complete control/snapshot integration,
retention, multi-node fault/Jepsen and production activation remain open.
Default legacy issuance/admission is unchanged; no deployment-readiness claim.

[chatgpt-codex-connector]

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

Reviewed commit: 67fc9b37d0

ℹ️ 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: 67fc9b37d0

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]

Checkpoint complete for exact last-push HEAD 67fc9b37d08424f52be8414f90264b7e54dc4d8c: explicit normal and security reviews pass, with no new current-head root inline findings. The prior phase-substitution finding was reproduced on d142, fixed with signed v3 creation-mode/phase binding, and its thread is resolved.

Every CI gate now passes: three-phase Go race including native large-value acceptance and unchanged full-length gRPC sequences; Jepsen encryption off/on; both Proto consistency runs; full lint/build; TLA; every CodeQL language and aggregate CodeQL; DCO and external status. The temporary CodeQL missing-Go-configuration warning cleared when Go analysis uploaded. No configuration bypass or test/assertion/deadline reduction was used. GitHub verifies the signed bootjp/contact commit.

This remains Draft and unmerged: production auth/registration and commit-time authority, all-member/future-member fences, unknown-attempt ingress journal, complete control/snapshot integration, retention/recovery and activation/performance gates are still open. Default legacy issuance/admission remains unchanged. Component qualification is not operational readiness or complete design implementation.

[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 (1c98487):

• distribution/bootstrap_plan.go
• distribution/bootstrap_plan_test.go
• store/lsm_store.go
• store/mvcc_store.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

Please review latest HEAD 1c98487 as a Draft foundation. Check the atomic data-group binding primitive and revised design contract. The physical-band issuer, trusted admission, and cross-group primary proof are explicitly not implemented or activated; do not treat this PR as closing the legacy range-validation hole.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 1c9848751b

ℹ️ 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: 1c9848751b

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 (d907d7f):

• distribution/bootstrap_plan.go
• distribution/bootstrap_plan_test.go
• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.go
• store/lsm_store.go
• store/mvcc_store.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: Didn't find any major issues. 🚀

Reviewed commit: d907d7f79d

ℹ️ 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: d907d7f79d

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]

@codex review

Please review the current pushed HEAD 1c4d687. The prior review receipt covered an older commit. The Ubuntu job failed in the external-rotation shutdown lifecycle test; that test passed 10/10 locally on this exact HEAD, and the failed CI job is being rerun.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Swish!

Reviewed commit: 1c4d687f59

ℹ️ 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: 1c4d687f59

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 (ba554ba):

• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.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

Please review latest pushed HEAD ba554ba. It fixes the P2 physical-band minimum boundary by advancing to the next millisecond when the current band cannot fit the batch, while still enforcing the committed ceiling. The physical-band race tests passed 3/3; CI for this new HEAD is starting.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Hooray!

Reviewed commit: ba554baec8

ℹ️ 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".

[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 (4e6cb9d):

• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.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

Please review the final pushed HEAD 4e6cb9d. It includes the physical-band boundary fix and removes real-clock adjacency from the rollover test. All TestTSOPhysicalBand tests passed with -race -count=3. Prior inline findings have been answered; new CI is running.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Nice work!

Reviewed commit: 4e6cb9d886

ℹ️ 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: 4e6cb9d886

ℹ️ 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.

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security: Keep disabled binding fields deterministic across versions

During a rolling upgrade with an old leader, a final-tree follower, and a caller able to reach Internal.Forward (peer auth is off by default), a handcrafted Request field 9 is unknown to the old binary, survives clone/proto.Marshal, and is applied there. Final-tree replicas recognize it here and route it to applyTimestampBoundCreation, which rejects it while timestampBindingEnabled is false. Etcd still advances the applied index for this non-HaltApply response, so one committed entry mutates old replicas but not new ones. Treat field 9 as legacy/ignored until replicated all-member activation makes interpretation uniform.

Useful? React with 👍 / 👎.

[bootjp]

Fixed in 1988168. Until replicated activation, the FSM now ignores binding field 9 for both single and batched apply, matching old-binary legacy behavior; public StampTimestampAdmission still rejects new bound requests. Memory/Pebble disabled-mode regression and full kv -race tests pass.

[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 (1988168):

• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.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

Please review latest pushed HEAD 1988168, including the security fix for mixed-version field-9 application. The FSM treats binding fields as legacy/ignored while activation is disabled, both for single and batched entries; public admission still rejects new bound requests. Disabled-mode memory/Pebble regressions and full kv -race passed. CI is restarting on this HEAD.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Can't wait for the next one!

Reviewed commit: 1988168ab3

ℹ️ 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: 1988168ab3

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]

@codex review

Please review latest pushed HEAD 507d96e. Code remains the security-reviewed 1988168; this push only documents inactive binding compatibility and physical-band rollover in the design doc. Full kv -race passed, and CI is running for this exact HEAD.

[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 (507d96e):

• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.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. Another round soon, please!

Reviewed commit: 507d96e551

ℹ️ 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: 507d96e551

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]

@codex review

Please review latest pushed HEAD 76014f6 after merging current main, including the sharded CI workflow and #1421 SQS test fix. The timestamp-binding and physical-band changes are unchanged from the last reviewed HEAD; focused TSO/FSM -race tests passed on this merge. New CI is running.

[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 (76014f6):

• kv/fsm.go
• kv/tso_raft.go
• kv/tso_raft_band.go
• kv/tso_raft_band_test.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. Hooray!

Reviewed commit: 76014f6bae

ℹ️ 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: 76014f6bae

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.