il2al: host function rules become two independent conditionals and ignore the new store s' #2279
Description
I came across this while looking at how il2al uses Either for nondeterminism.
The rules Step/call_ref-hostfunc-res and -div (added in #2210) can both apply:
spec/specification/wasm-3.0/4.3-execution.instructions.spectec
Lines 184 to 198 in 8d6a3af
--prose gives:
13. If an element of $hostcall((_HOSTFUNC hf), s, val^n) is some RES, then:
a. Let (RES s' result) be an element of $hostcall((_HOSTFUNC hf), s, val^n).
b. Execute the sequence $lift_result(result).
14. If BOT is contained in $hostcall((_HOSTFUNC hf), s, val^n), then:
...
- Steps 13 and 14 are not alternatives, so when both apply the algorithm does both.
s'is never used, so the store is not updated.
I would expect something like this, as for memory.grow (not sure how AL should update the whole store):
13. Either:
a. Let (RES s' result) be an element of $hostcall((_HOSTFUNC hf), s, val^n).
b. Update the store s to s'.
c. Execute the sequence $lift_result(result).
14. Or:
...
It seems il2al produces Either only for rules without conditions (translate.ml#L1155).
Note: This might be low priority since neither the document nor the reference interpreter uses this algorithm.
Activity
tamaroning commentedon Oct 14, 2026
@zilinc Since these rules came from #2210, I'd appreciate your thoughts on this.
zilinc commentedon Oct 15, 2026
I can totally believe that the the prose generator may give suboptimal or even wrong output at times. The AL pipeline is by and large by-demand, meaning that we try to ensure that it works for the things that will go into the official document. Since this part of prose isn't used in the official spec, it could be wrong. Unfortunately I think it will remain this way for the near future. Regarding if vs. either, I'm not entirely sure. From the SpecTec formulation, at least, it appears that there's a subtle difference. Here, algorithmically, the nondeterminism comes from the host function call, and "we" don't get to make the choice. Whereas for the
growinstructions, "we" can decide which choice to make. So maybe AL is right here to generate "if".rossberg commentedon Oct 15, 2026
Like @zilinc says, the prose backend obviously isn't prepared well for dealing with cases like this.
I agree that something closer to your second formulation would be adequate, with the modification that the possible choices still somehow need to be conditioned on what is in the set of possible non-determinisitc behaviours, like in the first formulation. Something along the lines of
a. Let (RES s' result) be an element of $hostcall((_HOSTFUNC hf), s, val^n).
b. Update the store to s'.
c. Execute the sequence $lift_result(result).
...
@zilinc, I don't think there is a difference in the flavour of non-determinism here. In both this and other cases, some meta-level function expresses the entire set of possible behaviours, and then as a specification device, "execution" arbitrarily picks one.
rossberg commentedon Oct 15, 2026
Btw, I think the spec currently doesn't specify that the result of hf must be non-empty. I think it needs to be. (Theoretically, we could have a rule that traps in that case, but that wouldn't reflect any behaviour possible in reality.)
rossberg commentedon Oct 15, 2026
@zilinc, please see #2280.
zilinc commentedon Oct 16, 2026
Oh yeah you're right. I misread the
<-part.