VM should ensure that the last operation is a `HALT`

[plafer]

The processor should ensure to always insert a HALT (even when no padding is needed). We should also have a boundary constraint that ensures that the last statement is a HALT.

This is because our multiset checks (buses and virtual tables) assume that no multiset element can be generated/removed from the last trace row (and hence we need to ensure that the last operation in the trace is an END).