[spec] Fix state for expression evaluation (WIP)

[rossberg]

This fixes an oversight in the evaluation of constant expressions for Wasm 3.0, where allocations can now in fact cause modifications to the store.

This is WIP, the fix currently causes the interpreter to fail. @f52985, can you please take a look?

[f52985]

Fixed.

The issue was that the animation pass assumed only the last argument of a relational premise is the output argument.

This assumption held for the previous premise:
-- Eval_expr: z; expr ~>* z; val
where val is the only output.

It no longer holds for the updated premise:
-- Eval_expr: z; expr ~>* z'; val
where the last two arguments (z' and val) are outputs.

The animation pass has been updated to handle this generalized case.