notes mizzy.org

planは予測であり、真実はapplyが確立する

確認済み 出典: explorations/2026-06-11-world-acquisition-incremental-plan/README.md §4, §8 / explorations/2026-06-10-carina-type-system-type-theory/plan-as-compilation.md §7 作成

planはロックを取らず、applyがロック下で差分を再計算する。この契約を意識的に推すと、plan時のworldの鮮度は正しさの問題ではなくUXの問題だと正当化できる。planは安いキャッシュで即答してよく、正しさの担保はapply側の検証に一本化される。

plan — ロックなし 古いworldでよい 安いキャッシュで即答してよい TOCTOU窓 他の書き手が 世界を変えうる apply — ロック下 差分を再計算して検証 ここで真実が確立する planは予測にすぎない。手前のあらゆる近似は「速さとUXのための近似」に位置づけられる。
正しさの担保がapply側に一本化されているため、plan手前の高速化はすべて契約を変えずに体感だけを変える最適化になる。

これは楽観的並行性制御(OCC)そのものの形である。OCCは「古いスナップショットで作業を進め、コミット時に検証する」枠組みであり、planが古いworldで動きapplyがロック下で再計算するCarinaの構造はすでにこの形をしている。リソース単位のversion比較(compare-and-swap的なapply)まで細粒度化する余地もある。

この契約が要請される根本の理由は、ターゲットが生きていることにある。通常のコンパイラのターゲットは受動的なメモリだが、IaCではコンパイル(plan)と実行(apply)の間に他の書き手が世界を変えうる。planがロックを取らない設計 — TOCTOU窓 + ドリフト警告 + apply側での再計算 — は、「IRは予測にすぎず、真の整合性は実行直前に再確立する」という、共有可変ターゲットに対する妥当な妥協である。

この読みは実務的な帰結を持つ。world取得を速くするためのあらゆる近似 — 排他所有による読み飛ばし、イベント駆動のdirty追跡、有界の古さを許すキャッシュ — は、契約を変えずに体感だけを変える種類の最適化として正当化できる。planの鮮度はapply直前の再読・検証で最終担保されるため、その手前はすべて「速さとUXのための近似」と位置づけられるからである。

#plan #apply #occ