Fix Wasm-1.0/2.0 spec

[f52985]

This PR introduces following changes for Wasm 1.0 / 2.0 specs.

1. Inject parenthesis at x* x'** properly so that they are correctly parsed (This issue seems to be happening repeatedly. Perhaps, changing parser so that they are parsed as intended even without parenthesis would be a better option in long term.)
2. Change instrX* into exprX at instantiate function
3. Change Step_read rule premises into Eval_expr at instantiate function. (Step_read requires exactly one reduction step to occur, i.e., disallows already-value instructions like I32.CONST 0.)

[rossberg]

Thanks!

[rossberg]

Declaratively, it would be more natural to have this more general relation (while leaving Eval_expr as is except invoking Steps):

Suggested change

	rule Eval/done:
	z; val* ~>* z; val*
	rule Eval/step:
	z; admininstr* ~>* z''; val*
	-- Step: z; admininstr* ~> z'; admininstr'*
	-- Eval: z'; admininstr' ~>* z''; val*
	relation Steps: config ~>* config hint(show "E")
	rule Steps/refl:
	z; admininstr* ~>* z; admininstr*
	rule Steps/trans:
	z; admininstr* ~>* z''; admininstr''*
	-- Step: z; admininstr* ~> z'; admininstr'*
	-- Steps: z'; admininstr' ~>* z''; admininstr''*

Would that work in the backend as well?

[f52985]

Yes, it should work well without any problem.

(It was already handled in hardcoded way. The rule premise Eval_expr: lhs ~> rhs is rougly translated to the AL statement 1. Let rhs be the result of computing $eval_expr(lhs), where eval_expr is a manually written algorithm)

[f52985]

I pushed a new commit introducing Steps relation.

[rossberg]

Nit: move up to other relations.

[f52985]

In that case, should I also move rules for Steps above rules for Step?

[rossberg]

I would move the relation decl after the others, so the rules can stay here, I think.

[f52985]

Oh I see, I thought you meant moving Steps relation above other Step relations.

[rossberg]

Same here.