Changed the input and output of all machine operations to be B0 compatible. We still deal with ATOMS as intermediate data within the specifications.
Added assertions to DecompConstants in the hope that it will help with some proof obligations.