Manuscript En03-A@1 · En03-A.tex · assumption · 5398614e
Assumption: Spectator-blind control
Typed interfaces and semantic configurations › Complete control and resource accounting · lines 555–574
En03-A@1#ass:sched
For the compared executions, inaccessible spectators do not change:
the selected command or its declared matter channel;
guard, applicability, or capacity-check results;
the support, block membership, or transport of original names;
successor control and declared resource data.
The controller is a specified function of the complete declared inputs. Equal such inputs select the same update and certificate. No undeclared spectator-dependent input is available to it.
The location transports are defined on all permitted spectator locations, and spectator storage and transport history have separately reserved resources sufficient for the compared run.
Randomized controllers are aligned using a common input-independent seed, or a specified coupled law satisfying the same equality property.