ortac-qcheck-stm: print which invariant failed and more details about the failure

Qheck-stm prints something like this (where I introduced a bug deliberately to make it fail):

generated error fail pass / total     time test name
[✗]    1    0    1    0 / 1000     0.0s Varray_spec STM tests

--- Failure --------------------------------------------------------------------

Test Varray_spec STM tests failed (15 shrink steps):

   push_front '\192'
   pop_at 0
   pop_front

+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Varray_spec STM tests:

  Results incompatible with model

   push_front '\192' : ()
   pop_at 0 : Ok (Elt '\192')
   pop_front : Ok (Elt 'a')
================================================================================

I can probably guess at which function failed (it is the last one), but I don't know from that message which postcondition failed, and what the values were (real run vs model) to debug it.

The monolith plugin prints something like this (on another test) that is better, because it shows the invariant that failed:

Runtime error in function `mem'
  - the invariant
      `b <-> mem i bv'
    was violated in the post-state.(* @02: Failure in an observation: candidate and reference disagree. *)
          #require "monolith";;
          module Sup = Monolith.Support;;
(* @01 *) let (Ok set0) = Sup.Exn.handle (create is Ok) 21;;
(* @02 *) let (Error _) = Sup.Exn.handle (mem is Ok 15) set0;;

Ideally the error message should include both sides of an invariant that failed so the developer can quickly see what the actual values causing the failure were.

I know that qcheck-stm only allows to return a bool, however QCheck itself does have a way to report more details that I just discovered recently: https://ocaml.org/p/qcheck-core/0.21.2/doc/QCheck2/Test/index.html#val-fail_reportf Using QCheck2.Test.fail_reportf you can format a string with the actual failure and quickcheck will show that instead of just the very generic 'test failed'.

I thought that perhaps using the 'wrapper' plugin might help (which does generate the Violated_invariant reports with proper strings), but that doesn't quite work yet:

File "examples/varray_spec_wrapper.ml", line 181, characters 19-22:
181 |      try insert_at t_5 i_1 x_4
                         ^^^
Error: This expression has type 'a Ortac_runtime.Gospelstdlib.sequence ref
       but an expression was expected of type 'b t

Would be nice if the reporting code could be unified across the 3 plugins, that way all 3 would get any improvement made in one of them (even if the actual reporting might have to be plugin specific, e.g. rewrap the ortac runtime error with the QCheck one)

ocaml-gospel / ortac

ortac-qcheck-stm: print which invariant failed and more details about the failure #188