[spec] `type` field of element instance seems unnecessary

[f52985]

Currently, the element instance consists of two fields, type and elem:

However, it seems that the type field of the element instance is unnecessary. As far as i know, none of the reduction rules for the execution actually access the type field of a element instance (only elem field is being accessed). Also, the elem.drop instruction is treating element instance as if it has only one field:

Does this type field of element instance have a specific purpose? If not, should it be removed from the spec?

[rossberg]

There are a few types in instance objects that aren't used in the reduction semantics directly, but are needed in the definition of well-formed store, and hence soundness, IIRC. Global instances are another such example.

But yes, the rule for elem.drop is missing the type. Would you volunteer to create a PR? :)

[f52985]

If "definition of well-formed store" refers to the section external typing, then type of global instances are indeed used here. However, I think that element instances are not the case, as element instances are not exported or imported. (And it seems that there isn't any other validation rules that uses runtime instances) I'm afraid I might be missing a rule that uses this field, but still somewhat confident that that's not the case.

Also, the element instance of reference interpreter also does not have type field: it only has refs.

Of course, regardless of being used or not, the element instance having a type field dose not harm the specification. I just want to know whether the type field of element instance is really necessary, and if it turns out that it is not the case, whether we still want it in the spec.

(And yes, I am willing to create the PR, as soon as my curiosity is resolved :))

[rossberg]

I meant Store Validity, and particularly, this judgement in the appendix. Funnily, the heading of that section also is missing the type. :)

This is needed to specify what a well-formed store is, which in turn is needed to prove soundness. In particular, this definition is also used indirectly to constrain what host calls can do to the store.

FWIW, there are also ideas about making segments im/exportable. :)

[f52985]

Oh, I see. I missed that there was the appendix for the soundness.

l'll create the PR that fixes both elem.drop, and the header of the judgement!