Commit-Window Observation Contracts for Reactive Entity-Component Systems

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.