排他所有が証明できれば読まなくてよい
worldを速くする三つの攻め口のうち、最も踏み込んだものは「読まなくてよい条件を作る」である。自分しか書かないリソースについては、自分の記録が真であり、クラウドAPIを叩く必要がない。
古典的な対応物はリース(Gray & Cheriton)である。「期限付きの所有権があるあいだは、再確認なしで自分のキャッシュを信じてよい」。IaCでは「このstateの所有者だけがこのリソース群を書く」という運用前提がリースに当たり、前提が成り立つ間はrefresh自体が不要になる。
型システムの角度から見ると、これはRustの所有権が「排他なら同期不要」をコンパイル時に証明するのと同じ形である。リソースごとに「書き手は誰か」を宣言のレベルで持たせ、自分(このstate)が排他所有するリソースはrefresh不要(自分の記録が真)とし、共有(コンソール操作や他パイプラインがありうる)と宣言されたリソースだけをイベント購読や同期GETの対象にする。
この宣言は単なる自己申告に留めなくてよい。IAM / SCPで「このロールしか書けない」が実際に強制されていれば、排他所有は運用上の仮定ではなく検証可能な前提になる。並行プログラム検証のrely-guarantee推論 — 環境の干渉をこの範囲と仮定して証明する枠組み — のIaC版である。
宣言された前提を機構で裏づけるこの形は、公称軸の部分型付けと同じ設計の型である。名前で宣言された区別を、その名前が指す実体の側で保証する。
根拠の確度
リース、rely-guarantee推論への言及はAIの学習データ由来で一次ソース未確認。IAM / SCPによる排他所有の強制が実際にどこまで検証可能な前提になるかは実装・実測を伴わないアイデアの段階。