驗證設計租約

crates/server/tla/DesignLeases.tla 是一個 TLA+ 模型，模擬了兩台共享一個儲存空間的 Finite 伺服器，以及一個在它們之間移動的設計 (design)。TLC（TLA+ 模型檢查器）會在有限的範圍內窮舉所有可能的步驟順序，並檢查兩條規則：

StoredEditsStay（隔離規則）：一旦儲存空間接受了一個編輯，任何其他伺服器上的過期副本都不能再覆蓋它。如果此規則被破壞，一個發生故障的伺服器重新啟動後，可能會清除新擁有者保存的編輯。
AckedEditsStay（已確認編輯持久性規則）：一個被 MCP 工具報告為「已完成」的編輯，要么存在於儲存空間中，要么存在於一個仍能保存它的副本中，除非編輯被保存前其伺服器崩潰或租約過期。如果此規則被破壞，代理 (agent) 會被告知編輯成功，但隨後編輯消失，用戶端看到它不見了，而代理卻不知道。

目前的程式碼通過了第一條規則，但在第二條規則上存在四個已知的破壞方式，列於下方的「已知發現」中。

你的變更是否影響到這裡？

是的，如果你變更了下表中任何函數。每個模型步驟都對應著它所代表的程式碼，審查者可以同時打開兩者進行比對。

模型步驟	程式碼
`CallStarts`, `CallFindsHandle`, `CallLoads`, `CallEdits`, `CallReads`	`mcp/mod.rs` `design`, `edit_checked`; `api.rs` `open`; `hub/mod.rs` `Hub::open`, `handle_for`; `hub/design.rs` `DesignHandle::load`, `edit`
`SaveTakes`, `SaveWrites`, `SaveFenced`, `SaveFails`, `SaveReleases`, `SaveDrops`	`hub/mod.rs` `persist`; `hub/design.rs` `take_save`, `save_failed`
`Unload`	`hub/mod.rs` `Hub::sweep`; `hub/design.rs` `unload_if_idle`, `is_idle`
`TickRenews` … `TickDiscovers`	`hub/mod.rs` `Hub::tick`, `let_go`, `remove`, `drop_copy`, `discover`, `summaries`; `hub/design.rs` `retire`, `end`, `lease`
`Owns`, `LeaseLapses`, `HeartbeatExpires`	`cluster.rs` `Members::now`, `lapsed`, `renewed`, `Cluster::owns`, `owner`
`CanClaim`, `Claimed`, 儲存空間寫入	`postgres/mod.rs` `claim`, `save`, `append`, `release`, `held`; `store.rs` `trait Store`（記憶體中的共享儲存空間必須匹配）
`Start`, `Crash`	`hub/mod.rs` `Hub::shared`

路徑皆位於 crates/server/src/ 下。

同步提交：6606714。 這是模型最後一次針對此程式碼進行檢查的提交。若要查看該提交之後所涵蓋程式碼的變更，請執行：

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

如果差異影響了表格中的某個函數，請在信任測試通過之前，重新閱讀其旁邊的模型步驟。僅在你確認每個已變更的步驟仍與新提交中的程式碼匹配後，才在此檔案中向前移動同步提交。

執行檢查

crates/server/tla/check.sh          # 日常檢查，約需 2 分鐘
crates/server/tla/check.sh --full   # 加入 Finding4.cfg 和 AllFixes.cfg，約需再多 3 分鐘

該腳本在首次運行時會將 TLC（tla2tools.jar v1.7.4，已校驗 SHA-256）下載到 ~/.cache/finite。你需要 Java 11 或更新版本。每個設定檔在結果與當前程式碼記錄一致時會輸出 ok，否則輸出 FAIL。當規則被破壞時，TLC 的輸出（包含通往破壞點的最短路徑）會被保存為 crates/server/tla/<config>.out。Git 會忽略這些檔案。

設定檔	已開啟的修復	邊界	今日結果
`Fencing.cfg`	無	1 次編輯，1 次讀取，2 個句柄，最多 18 步的行為	通過，約 280 萬狀態，2 分鐘
`DesignLeases.cfg`	無	1 次編輯，2 個句柄	發現問題 1，數秒
`Finding2.cfg`	FixRetire	1 次編輯，2 個句柄	發現問題 2
`Finding3.cfg`	FixRetire, FixOrphan	2 次編輯，2 個句柄	發現問題 3
`Finding4.cfg`	+ FixStaleDrop	2 次編輯，2 個句柄	發現問題 4，約 1 分鐘
`AllFixes.cfg`	全部四個	2 次編輯，2 個句柄	通過，約 1,600 萬狀態，2 分鐘

每個設定檔都將儲存空間的 epoch 限制為 3，並且不包含崩潰或寫入失敗。讀取 (read) 是一個不加載編輯就能載入設計的調用，例如 MCP 讀取工具或檢視器的 socket。隔離規則 (Fencing) 需要一次讀取，因為只有當兩個調用都載入了設計時，才會存在過期副本。包含該次讀取的完整狀態空間在 30 分鐘內無法完成，因此 check.sh 使用 TLC 的迭代加深（-dfid 18）來運行：探索最多 18 步的所有行為。最短的過期覆蓋路徑需要 17 步。用於發現問題的設定檔會探索其邊界內的所有可能性。TLC 會在遇到第一個被破壞的規則時停止，因此每個問題設定檔會為其之前的問題開啟建議的修復。Fix* 常量是假設性的開關。當它們全部為 FALSE 時，模型就代表了當前的程式碼。

閱讀結果

請搭配 /statechart 技能閱讀每個結果。它會將 TLC 到破壞規則的最短路徑轉換為以簡單文字描述的編號步驟列表；而當設定檔通過時，它會繪製一張設計如何在伺服器之間移動的圖表。

當設定檔輸出 FAIL 時，請判斷 bug 是在程式碼中還是在模型中：

真正的 bug 會給出一條你可以在程式碼中重現的路徑。走過每個步驟，從表格中打開對應的函數，並檢查該步驟能否按該順序在程式碼中發生。然後，像下面的「已知發現」那樣，用程式碼的語言報告這條路徑。在檢查通過之前，不要削弱規則或邊界；除非有人要求，否則不要更改產品程式碼。
建模錯誤 會給出一個程式碼無法執行的步驟。例如：兩個本應在同一鎖（狀態互斥鎖、持久化互斥鎖）下運行的步驟，在模型中被分開了；模型步驟缺少程式碼應有的保護條件；或者心跳在續約後立即過期。請修正模型以匹配程式碼，並說明你修正了什麼。
Fencing.cfg 的破壞來自深度受限的運行，其路徑不會命名其步驟。要獲得一個命名的最短路徑，請使用廣度優先方式運行同一個設定檔：cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla。它會在第一次破壞時停止，這在「當你故意變更所涵蓋的程式碼時」的測試中大約需要 6 秒。
error 表示 TLC 沒有完成：存在解析錯誤，或某個動作未賦值的變數。請閱讀 .out 檔案。

一個 FAIL 結果，如果過去程式碼曾破壞該規則而現在通過了，那就是好消息。下方的「已知發現」表格顯示瞭如何記錄它。

當你故意變更所涵蓋的程式碼時

在同一次提交中變更模型步驟和程式碼，並保留命名該函數的註解。
如果你的變更修復了一個發現，請將修復作為程式碼直接放入模型中，而不是作為開關：刪除 Fix* 常量，使步驟的行為與新程式碼一致，並從所有設定檔中移除該開關。下一個發現的設定檔將成為預設設定檔，而 check.sh 將獲得新的預期結果。
在信任一個測試通過之前，請在一個草稿副本中故意破壞程式碼，在模型中鏡像該破壞，並檢查設定檔是否能捕獲它。例如，如果你從 PgStore::save 中刪除了 AND epoch = $3，並從 SaveWrites 中刪除了 x.ptok = store.epoch，那麼 Fencing.cfg 會破壞 StoredEditsStay 規則。一個你從未見過失敗的檢查不能證明任何事情。
執行 check.sh --full，然後向前移動同步提交。

已知發現

以下均是基於 6606714 提交的程式碼中的競爭條件。在每一種情況中，代理的工具調用都返回成功，但編輯卻消失了。

編輯落到了正在保存其最後一個快照的副本上。 伺服器 A 已載入設計，並且一個 MCP 調用已通過 Hub::open。伺服器 B 加入並贏得了設計的所有權（A 上的租約過期也會導致相同結果）。A 的 tick 調用了 let_go，因此 retire 將副本標記為 Retiring。保存任務的 take_save 獲取最後一個快照。然後調用的 DesignHandle::edit 獲取鎖並提交到這個正在退休的副本，因為 edit 從不檢查 life。保存任務保存了不包含該編輯的快照，釋放了租約，並且 drop_copy 清除了 pending。B 載入設計時沒有那個編輯。要在真實應用程式中觸發它，編輯必須在 tick 運行時已經在等待設計鎖，例如多個代理同時執行大型 write_html 調用。撤銷、重做、導入和評論更新也走相同的路徑。
編輯落到了中心樞紐 (hub) 已從其列表中移除的句柄上。 一個調用的 handle_for 返回一個尚未載入的句柄。B 加入，A 的 let_go 發現沒有載入任何東西，因此它調用了 remove。該調用的 load 聲明瞭租約並在該句柄上載入了副本。下一次 tick 的 loaded 列表來自中心樞紐的列表，而該列表已不再有此句柄。因此 tick 釋放了租約，副本的下一次保存失敗並返回 Fenced。這不需要停機，只需要一台伺服器加入。
tick 在讀取副本後，該副本被重新載入，然後 tick 將其丟棄。 單一伺服器，無成員變更。tick 讀取了 lease()（令牌 1）。然後設計卸載，一個調用重新載入它（令牌 2）並提交了一個編輯。tick 讀取了 held()（令牌 2），發現 2 ≠ 1，並調用了 drop_copy。drop_copy 終結了這個新副本，包括其中待處理的編輯。這個窗口只有兩次讀取之間的間隔，因此非常狹窄，但它在每次 tick 時都會運行。
一個剛剛續約了租約的伺服器提供了其過期副本。 B 停機超過其租約期限，A 接管了設計並保存了一個編輯。B 恢復。其 tick 續約了心跳，從那一刻起，Members::now 將 B 計為活躍且又是所有者。但 let_go 循環尚未運行。B 上的一個調用載入了仍然標記為 Live 的過期副本並提交了一個編輯，該編輯稍後會失敗並返回 Fenced。這需要先有一次停機。

AllFixes.cfg 為每個發現檢查了一個建議的修復：edit 拒絕一個不是 Live 狀態的副本（發現 1）或一個不在列表中的句柄（發現 2）。tick 僅在其令牌與它之前讀取的一致時才丟棄副本（發現 3）。一個在過期後續約的伺服器，在它完成 let_go 之前不會將自己計為活躍（發現 4）。使用全部四個修復後，AckedEditsStay 規則在這些邊界內得以保持。

不在本模型覆蓋範圍內的事項

單個設計、兩台伺服器、MCP 編輯。撤銷、重做、導入、註解和重新命名走相同的鎖定並提交路徑，但未被單獨建模。Hub::delete 也未建模。
文件儲存和 FINITE_NODES 交接（hand_off_one、adopt），以及路由器。
關機時的 Hub::flush、日誌壓縮閾值（COMPACT_AFTER、COMPACT_BYTES），以及 Recent（檢視器恢復的緩衝區）。
時序。TLC 會窮舉所有步驟順序，因此模型顯示了競爭條件的存在，而非其發生頻率。它假設伺服器自身的租約定時器（Members::lapsed）不會比資料庫將其心跳視為過期的時間更晚。這在兩個時鐘以相同速率運行時成立。
更大的邊界。更多的編輯、讀取、句柄或 epoch、崩潰和寫入失敗不在日常設定檔中。AllFixes.cfg 也曾經在 1 次編輯、1 次崩潰和 1 次寫入失敗（340 萬狀態）下通過。隔離規則 (Fencing) 在 18 步之後的測試尚未完成：在 1 次編輯和 1 次讀取的情況下，它通過了超過 5000 萬個不同狀態，並且仍在運行。不要信任一個沒有讀取的舊版 Fencing 測試：僅一次編輯只會載入一個副本，因此沒有東西會變為過期。

verify-design-leases