[spec] Define soundness rules in SpecTec

[rossberg]

Formulate extra rules from Type Soundness Appendix in SpecTec.

Fix SpecTec sideconditions pass to not generate vacuous iterated premises.

@f52985, the prose backend crashes failing to find one of the added relations. That may have to do with the preceding "Yet" warning from translate_rulepr, which IIUC means that something is unimplemented in the backend. Can you please have a look?

../../specification/wasm-latest/7.1-soundness.configurations.spectec:211.62-211.76: translate_rulepr: Yet `(fv_1, s, fv_2)`
Untranslated relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype)
Untranslated relation Instrs_ok2: `%;%|-%:%`(store, context, instr*, instrtype)
Untranslated relation Expr_ok2: `%;%|-%:%`(store, context, expr, resulttype)
../../spectec/spectec: uncaught exception Failure("Unknown relation id: NotImmReachable")

Backtrace:
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Backend_prose__Gen.prem_to_instrs in file "src/backend-prose/gen.ml", line 288, characters 16-58
Called from Backend_prose__Gen.prem_to_instrs in file "src/backend-prose/gen.ml", line 327, characters 42-61
Called from Stdlib__List.concat_map in file "list.ml", line 288, characters 32-37
Called from Stdlib__List.prepend_concat_map in file "list.ml", line 292, characters 20-46
Called from Stdlib__List.map in file "list.ml", line 85, characters 15-19
Called from Backend_prose__Gen.prose_of_rules in file "src/backend-prose/gen.ml", lines 432-434, characters 4-48
Called from Backend_prose__Gen.proses_of_rel in file "src/backend-prose/gen.ml", line 451, characters 23-70
Called from Stdlib__List.concat_map in file "list.ml", line 288, characters 32-37
Called from Stdlib__List.prepend_concat_map in file "list.ml", line 292, characters 20-46
Called from Backend_prose__Gen.prose_of_rels in file "src/backend-prose/gen.ml" (inlined), line 579, characters 20-48
Called from Backend_prose__Gen.gen_validation_prose in file "src/backend-prose/gen.ml" (inlined), line 583, characters 2-39
Called from Backend_prose__Gen.gen_prose in file "src/backend-prose/gen.ml", line 648, characters 25-48
Called from Dune__exe__Main in file "src/exe-spectec/main.ml", line 306, characters 18-54

[raoxiaojia]

A comment on the soundness appendix -- is there any plan of adding a definition for the validity of the typing context C itself (which probably just says that all types in C.Types are valid)? Unlike pre-3.0, the type system is quite rich currently, and C.Types can contain ill-formed types in itself (e.g. invalid deftypes/heaptypes etc). The validity of C is required to prove that intermediate matchings for deftypes/heaptypes are correct.

[rossberg]

@raoxiaojia, good point. Yes, at this point we need that, too. I'll look into it.

[rossberg]

@raoxiaojia, I just pushed a commit that adds a wf-rule for contexts. Can you please check if it makes sense to you?

[raoxiaojia]

@rossberg Looks mostly fine, except this line which I'm unsure:

-- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK n i)^(i<m)

I would have thought n is the starting offset of the rec group, which needs to increase per element in the group, so should it be OK (n+i) i? I've been learning the 3.0 type system stuff recently though so I could be wrong.