一句话：提出 RxTCoreECS 演算，形式化反应式 ECS 的提交窗口观察契约，并在 Rocq 中机器化验证其核心定理。
现代实体-组件系统（ECS）运行时通过结构事件（OnAdd/OnSet/OnRemove）、变更过滤器与持续查询（CQ）只重跑数据发生变化之处，但通知合并、提交窗口内对写不相交更新的重排、CQ 成员缓存、迭代至静默等底层优化的正确性一直缺乏明确语义。本文提出 RxTCoreECS 演算，把 Core-ECS 的 store-and-scan 基线与反应式事务层整合，用显式两层通知模型刻画提交窗口观察契约：事件式提交产生逐操作的顺序轨迹，净效应提交产生每单元增量（每个提交窗口内每单元至多一个事件）。作者定义了相对于入队前缀的窗口局部观察等价，仅在单个提交窗口内商掉事件顺序，证明写不相交条件下的调度独立性，并用合并精化与前向模拟定理连接两层。论文还给出带 Added/Removed/Changed 增量正确性引理的 CQ 缓存模型、显式暴露每窗口一次 bump 策略的版本/过滤器对齐定理、燃料有界的静默循环，以及在轮次精化与稳定性义务下可复用的 all-dirty 扫描闭包模式。所有形式定义与命名结论均在 Rocq 中机器化检验。
Modern entity-component systems (ECS) runtimes expose structural events (OnAdd, OnSet, and OnRemove), change filters, and continuous queries (CQ) so that systems rerun only where data changed; yet the correctness of the underlying optimizations—coalescing notifications, reordering write-disjoint updates within a commit window, caching CQ membership, iterating to quiescence—has lacked a semantics that states the required commit-window observation contract . We present RxTCoreECS , a calculus that formalizes this contract for reactive ECS by integrating a Core-ECS store-and-scan baseline with a reactive transactional layer. Its key design point is an explicit two-tier notification model: (i) an eventful commit that emits a sequential per-operation trace, and (ii) a net-effect commit that emits a per-cell delta (at most one event per cell per commit window). The target contract is intentionally windowed: observers are order-insensitive within a commit window, and Changed is a dirty-by-write post-membership filter rather than a semantic-equality test. We define a window-local observational equivalence, relative to the incoming queue prefix, that quotients event order only within one commit window, prove schedule independence under write-disjointness, and connect the two layers by a coalescing refinement and a forward simulation theorem. We add a CQ-cache model with correctness lemmas for Added/Removed/Changed deltas, an explicit version/filter alignment theorem exposing the once-per-window bump policy for touched entities and cells, and a fuel-bounded quiescence loop. We prove a reusable all-dirty scan-closure schema under explicit round-refinement and stability obligations. All formal definitions and named results in the paper are mechanized and checked in Rocq.
@article{paperbot12145,
title = {Commit-Window Observation Contracts for Reactive Entity-Component Systems},
author = {Tomoyuki Aotani and Tetsuo Kamina},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839467}
}