Scoru: forbid `Level_crossing` proof production when the payload is None
The follow-up issue created by Nicolas is the source of the issue:
The following discussion from !6130 (merged) should be addressed:
-
@naih started a discussion: (+1 comment) So one of the properties is about a dependency between a
proofand a messageserialized option, where it should be impossible to have aLevel_crossingwithNone.This sounds like an invariant that could be tracked by OCaml's typechecker with a GADT. Since the property is critical (or not?), should we consider a nice-to-have follow-up, or would it be overkill because of the overhead of GADTs in the code?
In the merge request, we forbid a Level_crossing proof with a None payload in verify_proof. However, we manage to create this kind of invalid proof by using produce_proof with a tweaked configuration. The best solution would be to type check this, which is doable.