Removing duplicate prose

As mentioned in #63, there were duplicate prose for:

warning: prose rule `exec/array.new_data` has multiple definitions
warning: prose rule `exec/call_ref` has multiple definitions
warning: prose rule `valid/cvtop` has multiple definitions

There were two reasons:

(1) Manually-written algorithms

Execution algorithms for exec/array.new_data and exec/call_ref are written manually in backend-interpreter/manual.ml, for translating them to AL were quite tricky. The problem was that the failed translation (indicated by YetI) from il2al/translate.ml and the manual algorithms were counted twice. Thus, I've modified exe-watsup/main.ml to nullify the failed translations for manual algorithms.

This resolves the upper-two warnings.

(2) Prefix validation rule names

When translating formal rules to prose, we first group validation rules by their name's prefix. For example, Instr_ok/select-expl and Instr_ok/select-impl are grouped by their prefix select-. The rule names for the validation of cvtop were not properly named with the same prefix, so I re-named them to: cvtop-reinterpret, cvtop-convert-i, and cvtop-convert-f.

This handles the last warning, so all warnings are now gone. Yet, the current validation prose generator cannot handle multiple validation rules per Wasm instruction. select and cvtop are such cases, where the generator only takes the first rule and translates it, ignoring the rest.

https://github.com/Wasm-DSL/spectec/blob/9a1f5646259961c9c3c52cae1dd1dc79b73e8052/spectec/src/backend-prose/gen.ml#L83

This should be addressed, but will take some time since this requires some discussion with @f52985.

Wasm-DSL / spectec

Removing duplicate prose #69