the soc.fu pipeline data structures have been designed to notify MultiCompUnit that they have data to be stored. this by setting Data.ok in their Output n.data_o members.
nuts. just realised that all the formal proofs - and unit tests - need to check XER.so ok, XER.ca ok etc. as well.