[spec] Missing admin lifting of `call_ref` and `return_call_ref`

[raoxiaojia]

call_ref/return_call_ref (3.0's invoke/return_inovke) seem to be missing a lift to instr_ok2 that works for general typeuses (in particular, deftypes) instead of just idx. This is a soundness gap only, since deftypes can only appear as their arguments during execution (via funcinst lookups), and the binary format only contains encodings for idx arguments.

The minimally sufficient fix is to add a rule for those 2 instructions carrying deftypes, since rec n genuinely cannot appear in the current opsem rules (I think). So something like this should work:

rule Instr_ok2/call_ref:
  s; C |- CALL_REF dt : t_1* (REF NULL dt) -> t_2*
  -- Expand: dt ~~ FUNC t_1* -> t_2*

rule Instr_ok2/return_call_ref:
  s; C |- RETURN_CALL_REF dt : t_3* t_1* (REF NULL dt) -> t_4*
  -- Expand: dt ~~ FUNC t_1* -> t_2*
  -- if C.RETURN = (t'_2*)
  -- Resulttype_sub: C |- t_2* <: t'_2*
  -- Instrtype_ok: C |- t_3* -> t_4* : OK

(I noticed that $expanddt was removed at some point, and all expansions now use the ~~ syntax instead).

Generalising it for general typeuses is also possible, but there seems to be no need for that.

[rossberg]

Indeed. Please see #2188 for a fix. I'm using Expand_use for proper abstraction.