Definition: Semantic admissibility

A semantically admissible update is

where each ${\Phi }_{s,b}$ is a complete channel between the declared input and output interfaces in $b$, satisfying Assumption ass:completecontrol.

Allocation, destructive readout, classical record creation and discard, and relocation of names and records are permitted only within $b$. No output of the block is placed outside $b$.