search

0xPolygonMiden / miden-vm

STARK-based virtual machine
MIT License
615 stars 152 forks source link

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

Open plafer opened 1 month ago

plafer commented 1 month ago

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).

bobbinth commented 1 month ago

Good point! I thought we already had this - but I guess since decoder constraints are not yet implemented in Rust, we didn't add any assertions against the decoder part of the trace.