To break the dependency cycle between the interpretation of operations
and the definition of the semantics of Michelson types, we rely on the
following stratification observation: data appearing inside operations
cannot contain operations because the operation type is neither
passable nor storable.