[go: up one dir, main page]

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 proof and a message serialized option, where it should be impossible to have a Level_crossing with None.

    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.

Edited by Valentin Chaboche