Improvements to IOSim compatibility

[MaximilianAlgehed]

This PR significantly simplifies the IOSim compatibility module by re-organizing StateModel to differentiate between the "model type" and the "perform type". One big plus of this is that we've won the ability to have models with different backends where the types might even by symbolic! (One can always hope!)

[MaximilianAlgehed]

@abailly Have a look at this - I think it's pretty cool how this works out!

[MaximilianAlgehed]

And yes, this is a major breaking change and we need to discuss how to best handle that. I also haven't finished everthing, but I think it's good getting a bit of a spotlight on this.

[ghost]

Could you elaborate on the reason behind those changes? I am a bit confused because we already use the StateModel in hydra along with IOSim and it works fine. Perhaps we are doing things in a naive way?

[MaximilianAlgehed]

Could you elaborate on the reason behind those changes? I am a bit confused because we already use the StateModel in hydra along with IOSim and it works fine. Perhaps we are doing things in a naive way?

Have a look at the changes to the registry example. To be able to write properties where the state isn't indexed by s (which you need to be able to work properly with DL properties) you need the state type not to mention the s parameter.

[MaximilianAlgehed]

@abailly-iohk do you know why the build isn't working?

[ghost]

It seems zlib-dev is missing but I don't understand why it fails now and wasn't before, you did not change anything in the dependencies. Adding mtl should not entail recompilation of the whole world. Don't bother with this, I can take care of turning it green later, once you're happy with the code and it builds locally.

[MaximilianAlgehed]

I think I'm pretty happy with the code now. I'll just bump the version and we can merge this.

[ghost]

I am still not entirely convinced we need the Realized typeclass to be part of the library: The Model should be completely independent of whatever Monad instance the RunModel is expressed in, and it should the latter's role to provide a translation layer which is specific to this execution engine. But I feel you know better so I will defer to your expertise.
Could you please update the CHANGELOG.md with some high-level statement about this change and also format the code with fourmolu for consistency's sake?

[MaximilianAlgehed]

@abailly-iohk I understand the concern about the Realized type family and splitting the postcondition out. However, I think the main arugments for this change are:

1. There is already a level of indirection in the library (Var) and you don't want to force every new perform to introduce its own indirection tricks to deal with this situation.
2. You want to make it possible to have many different runners - e.g. ST, IO, and IOSim or a concolic / symbolic testing engine and splitting out the postcondition allows you to have something like a symbolic postcondition that does something like SMT magic or an IO postcondition that queries the actual state of the system.

[MaximilianAlgehed]

Also the model is now completely independent of the monad that RunModel is expressed in!

What we could add back is a model postcondition. But since this would have to talk about the ideal return type of an action it's not clear what this would mean. It's certainly not clear that you can always obtain a value of the ideal return type (e.g. in a symbolic or IOSim runner).

[ghost]

Interestingly, we now have a failing test: https://github.com/input-output-hk/quickcheck-dynamic/runs/8183759215?check_suite_focus=true#step:7:36 🎉 🤔

[MaximilianAlgehed]

Interestingly, we now have a failing test: https://github.com/input-output-hk/quickcheck-dynamic/runs/8183759215?check_suite_focus=true#step:7:36 🎉 🤔

Yes! That's on purpose ;) We could disable that test for now and I'll submit a new PR that turns it on. A fix to this failing test will hopefully be merged in io-sim soon:
input-output-hk/io-sim#19

[ghost]

Understood. But then we can expect the failure so that it now passes and when iosim gets updated, it will fail again?

[MaximilianAlgehed]

When io-sim is updated we need to change the implementation of the Registry example a bit because io-sim is currently lacking threadStatus and we need it to correctly implement the example. So nothing will be "automatic" as it were. Easiest solution here is just commenting it out and as soon as the other PR is merged in io-sim I make the necessary changes to the example and add in the tests.

[github-actions]

Unit Test Results

0 tests   - 1   0 ✔️  - 1   0s ⏱️ ±0s
0 suites  - 1   0 💤 ±0 
1 files   ±0   0 ❌ ±0 

Results for commit 7e3b5b6. ± Comparison against base commit f2c8c85.

♻️ This comment has been updated with latest results.

[MaximilianAlgehed]

Waiting for it to turn green and then I'll merge and get started on the fourmolu PR.