The Tydi (Typed Dataflow Interface) specification was introduced to bridge a gap in the High Level Synthesis (HLS) domain, enabling engineers to easily define component interfaces, mapping com- plex, dynamically sized data structures onto hardware streams. While Tydi successfully defines the static bit-level layout, it lacks a formal description for the dynamic procedure of mapping elements in a stream onto hardware lanes. This ambiguity has hindered the development of Tydi related tools and its integration in HLS frameworks. This work introduces a layered formalism for Tydi, centred around a modular operational semantics. It defines a two-tiered type system that separates a flexible user- facing syntax, from a canonical, hardware-oriented representation, strengthening the link between a type’s composition and runtime behaviour. The dynamic mapping is implemented by a configurable set of small-step semantics rules. These are derived from a user-provided set of formal properties, replacing the specifications' monolithic complexity levels with fine-grained control over interface logic. We define key structural determinism and progress metrics for the formalism, enabling the verification of interface implementations for streams of arbitrary type. This foundation enables developers to de- fine verifiably correct, typed hardware stream interfaces as easily as software, while retaining control over critical engineering trade-offs. A simulator of the semantics has been implemented, and provides empirical verification of the formalism and an insightful overview of the parsing logic.