New encodings have been proposed in the aborting RO paper.
We should consider implementing and benchmarking them, especially in combination with leanVM.
I currently think that these can simply be added by implementing a new instance of the message hash trait and using it in combination with the target sum encoding (essentially as described in the paper).