Pipelining: improve quality assurance

So far, for the Pipeline part 1 (!5557 (merged)) we have:

• Documentation:
  • The code and tests come are documented.
  • Several working documents that deal with previous code analysis and invariant definitions
• Validation
  • regression unit tests: validate_operation makes the same checks as precheck used to do. Those tests cover all kinds of manager operations, but run on one specific input set (for context and operation parameters).
  • new feature tests: !5614 (merged) introduces those tests, covering only one kind of manager operations but running on one specific input set (for context and operation parameters).
  • replay tests: via tezos-node replay command and a tweaked apply (see: vicall@pipelining@precheck-to-validate)

In terms of quality assurance, stronger confidence in the code requires:

• Doc/spec:
  • provide the rational cf. #3243 (closed)
  • normalize the doctrings up to guidelines,
  • generate ocaml doc from those docstrings even in ml file, and introduces them as specification.
• Validation
  • unit tests
    • Complete 1m/validate unit test with baker 1M and run_operation on batch with several sources,
    • Enforce 1m/validate unit tests in terms of manager kind and mode coverage,
    • Enforce unit test coverage on operation parameters via pbt
    • Enforce unit test coverage on context via fuzzing,
  • integration tests:
    • Baker: tezt + baker client and/or lib delegate,
    • RPCs: suite complete pour ces 3 rpc via tezts +
    • node: prevalidator
  • model-based testing:
    • implement a reference implementation,
    • formally verify this reference implementation,
    • test that on the same inputs, we can make the same observation for the concrete and reference implementation