Rule prose with state variable z

[jaehyun1ee]

This adds the state variable z to rule prose.

What has changed

Previously, we have removed all state variable z from the prose, for the store s in z is regarded as an implicit global variable throughout the prose semantics. This has incurred problems when rendering the prose, for the removed z caused arity mismatch on applying the display hints.

For example, below is the generated spec document before this PR. The prose calls $funcaddr with no argument, so the display hint, z.module.func is not applied. This happens throughout many helper function (getters and setters for notational shorthand) applications.

With this PR, the IL-2-AL phase does not remove the state variable z. Thus, display hints with z now works well in rendered prose also. For all generated prose from the reduction rules that use z, an instruction "Let z be the current state.` is added as the first instruction.

What should be addressed afterwards

Yet, the AL interpreter still works on the assumption that the state variable z is removed during IL-to-AL.
Thus, after generating AL from IL, the interpreter backend runs one last pass that removes the state variables, and the prose backend runs one last pass that adds the instruction "Let z be the current state."
The immediate result is that there is a slight difference between what is seen (prose backend) and what is executed (interpreter backend).

We plan to work on reconciling the two in a separate PR, i.e., adjust our AL interpreter so that we can get to execute the rendered prose by handling the state variable z somehow.

[rossberg]

Looks good to me.

As a separate change, the "ref.func ..." should probably be rendered with the parentheses.

Also, can we render |...| in prose, as "the length of ..."?

[jaehyun1ee]

As a separate change, the "ref.func ..." should probably be rendered with the parentheses.

This is handled in the latest commit: Add parentheses to EL SeqE when translated from AL CaseE.

Also, can we render |...| in prose, as "the length of ..."?

This is somewhat complicated, for there are AL expressions in the form (I32.CONST |$arrayinst(z)[a].FIELDS|).

rule Step_read/array.len-array:
  z; (REF.ARRAY_ADDR a) ARRAY.LEN  ~>  (CONST I32 $(|$arrayinst(z)[a].FIELDS|))

It relates to the discussion made in #61, but I am not sure how the render_expr' should print this as a mixture of English and math formula.

Or, we can add a hacky pass on AL, such that if there is an occurrence of LenE used in CaseE, then we insert a LetI instruction that binds the CaseE to some VarE.
e.g.,

execution_of_ARRAY.LEN
1. Let z be the current state.
2. Assert: Due to validation, a value is on the top of the stack.
3. Pop the value admin_u0 from the stack.
4. If admin_u0 is of the case REF.NULL, then:
  a. Trap.
5. If admin_u0 is of the case REF.ARRAY_ADDR, then:
  a. Let (REF.ARRAY_ADDR a) be admin_u0.
  b. If (a < |$arrayinst(z)|), then:
    1) Let **foo** be the length of $arrayinst(z)[a].FIELDS.
    2) Push the value (I32.CONST **foo**) to the stack.

[rossberg]

Yeah, this is not high priority, but eventually I'd prefer to have something like that. (Of course, the condition should ideally read "a is smaller than the length of $arrayinst(z)" and be an assertion. :) )

[jaehyun1ee]

Thank you for the comments :)

I'll merge this with two things in mind,
(1) Later we will reconcile the prose and interpreter backends to work on the same AL
(2) Properly render LenE as "the length of ...", either by a pass on AL or some smart way to introduce validation assertions

[rossberg]

Yes, more generally, it should be possible to implement an AL-to-AL pass that performs a kind of normalisation, such that it lifts out complex subexpressions (of various shape) and names them. Sort of like a partial A-normal form.