[WIP] PoC for trace validation

[bugarela]

Hello

This is a PoC I've started to enable Quint to reproduce the steps/states taken in a given ITF trace. This considers any nondetPicks present in the trace, and tries to guess the other ones.

We should move this to rust. I wrote this last year.

This doesn't do anything special with any and actionTaken yet, but we could.

The diffs thing is something I was exploring as a way to report mismatches, but we need to think harder about what we want there.

Experiment

Using the tendemint example from choreo (I'm currently at 0f41da72):
https://github.com/informalsystems/choreo/tree/main/examples/tendermint

Step 1: generate an ITF trace from tendermintMicro with --mbt. This should be the same as getting a trace from an ideally-structured implementation.

quint run --main valid tendermintMicro.qnt --max-steps=50 --out-itf trace.itf.json --mbt --max-samples 10

Step 2: Do the refinement mapping by hand, converting fields from one model to another. In this case, we only have to delete some "tracking" fields that are not part of the base model, which I do via CLI jq. The var names in Quint traces also don't completely match the ones in the model (feature or bug?), so we need to convert them:

jq '
  .states |= map(
    # 1. delete the four fields inside each process
    (.["tendermint::choreo::s"].system."#map") |=
      map( [.[0], (.[1] | del(.proposals, .prevotes, .precommits, .decisions))] )

    # 2. rename "tendermint::choreo::s" → "s"
    | .s = .["tendermint::choreo::s"]
    | del(.["tendermint::choreo::s"])
  )
' trace.itf.json > transformed.itf.json

Step 3: Use --in-itf to replay the trace

quint run --main valid tendermint.qnt --max-samples 1 --max-steps=100 --in-itf transformed.itf.json --mbt

This is resulting in a mismatched at this point. The diff gets messed up by the progress bar, but it might be related to a need of allowing stuttering steps. The "micro" version will take several steps until the abstract model makes a step, and I think we are not yet considering this scenario.

You also change some random value in first states of the transformed.itf.json and check if this can catch it:

[simk185]

Hey!

I've tested this trace replay on a Paxos trace and i ran into similar issues.
I've created a very short paxos trace using
quint run --main Paxos_val2_accept3_quorum2 Paxos.qnt --max-samples 1 --max-steps 5 --out-itf traces/small_trace.itf.json --mbt
and sanatized it, getting rid of "Paxos_val2_accept3_quorum2" prefixes of the variables.
When using
quint run --main Paxos_val2_accept3_quorum2 Paxos.qnt --max-samples 1 --in-itf traces/small_trace_sanitized.itf.json --mbt to replay this trace, i got the following error (i've tried reconstrcuting it, removing the progress bar:

Paxos.qnt:117:7 - error: [QNT000] Failure replaying trace
117:       msgs' = msgs.union(Set(m))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^
Set(
  Msg1a(
    {
      bal:
        4612970647851436625385475460398140283625135723862570152993320511035231860550
    }
  ),
  Msg1a(
    {
      bal:
        21762449469317047431804584301429585668444687014191936236574085063588135625343
    }
  )
)
error: Runtime error