[spec] Define soundness rules in SpecTec

[rossberg]

Formulate extra rules from Type Soundness Appendix in SpecTec. Also closes #2141.

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?

Upd: I guess using OK n i is saying that the REC group cannot access any types in the same group using _IDX, which might be intended, since all subtypes should already be rolled (IDX replaced with REC) at the point of validating the group (which populates the C.REC entries). In comparison, the current statement of rectype_ok2 allows this shifted offset per element:

rule Rectype_ok2/empty:
  C |- REC eps : OK x i

rule Rectype_ok2/cons:
  C |- REC (subtype_1 subtype*) : OK x i
  -- Subtype_ok2: C |- subtype_1 : OK x i
  -- Rectype_ok2: C |- REC subtype* : OK $(x+1) $(i+1)

but that seems to be also fine because rectype_ok2 may need to handle pre-rolled types.

[rossberg]

You're right, thanks for spotting! Fixed.