[spec] Define soundness rules in SpecTec

[rossberg]

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

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.

[raoxiaojia]

@rossberg @zilinc mentioned that the fix for rectype_ok was not synced to 3.0 yet (only on latest) -- just checking that the soundness section is intended to be part of the 3.0 spec as well?

[zilinc]

@rossberg @zilinc mentioned that the fix for rectype_ok was not synced to 3.0 yet (only on latest) -- just checking that the soundness section is intended to be part of the 3.0 spec as well?

At least I can see 2.1 in wasm-3.0 and latest are done differently.

[rossberg]

Ah, sorry, propagated now.

[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?

Yes, the prose generator was somewhat overfitted to specific relation forms. I have fixed it so that it can robustly handle the new relation formats. The rendered prose is still somewhat naive and may occasionally require a prose hint, but the generator should no longer crash in most cases.

[rossberg]

Hi @f52985, thanks for the hotfix! That works, but when I renamed ImmReachable to ImmutReachable, it crashed again. I was able to work around that by adjusting valid_helper_relations. Two questions for further improvements, though:

• Can we make it not crash, but output an error message, ideally with advice on how to fix the error?
• Would it be possible to get rid of the hard-coded relations list in favour of either using hints, or even better, compute the list automatically by taking the dependencies of relations using |-?

[f52985]

• Can we make it not crash, but output an error message, ideally with advice on how to fix the error?
• Would it be possible to get rid of the hard-coded relations list in favour of either using hints, or even better, compute the list automatically by taking the dependencies of relations using |-?

Done. Now it automatically detects the validation rules, based on the dependencies, removing all the hardcodings.

[rossberg]

@f52985, oh excellent, thanks for the super-fast granting of my wishes! Since this PR already landed, can you please create a new one with that change?

[f52985]

Sure, I opened the new PR: #2147