Backingstore-agnostic property tests using model-based testing

[jorisdral]

Description

Resolves #3954.

Previously, the BackingStore functionality was only being tested through higher-level tests like the OnDisk tests. This PR introduces QSM property tests that exercise the BackingStore API directly. The tests can be reused for any type of backing store that implements the BackingStore API. As a result of these tests a bug was identified in the implementation of range reads for the LMDB backing store. This PR also fixes this bug by re-implementing the range reads using a new LMDB cursor monad that is introduced by a PR in the lmdb-simple package: input-output-hk/lmdb-simple#1

Update 2022-12-05

Since the last review round, the tests have been refactored to use quickcheck-lockstep instead of QSM. Furthermore, the LMDB and InMem backing store have seen some refactoring as well. Changes include:

1. For both backing store implementations, we improved their behaviour in case of errors.
2. The LMDB backing store now uses the cursor API to perform range reads.
3. Communication between the LMDB backing store and LMDB bindings now runs through the LMDB.Bridge module.
4. We created an alternative to the Transaction type from the LMDB bindings that keeps open a transaction handle for as long as we need it to.

Checklist

• Branch
  • Commit sequence broadly makes sense
  • Commits have useful messages
  • New tests are added if needed and existing tests are updated
  • If this branch changes Consensus and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If this branch changes Network and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If serialization changes, user-facing consequences (e.g. replay from genesis) are confirmed to be intentional.
• Pull Request
  • Self-reviewed the diff
  • Useful pull request description at least containing the following information:
    • What does this PR change?
    • Why these changes were needed?
    • How does this affect downstream repositories and/or end-users?
    • Which ticket does this PR close (if any)? If it does, is it linked?
  • Reviewer requested

[dnadales]

Thank you for adding this test 🙏 Looks great, I left some comments and to merge this I think we should:

• Address the FIXMEs.
• Perform coverage testing to make sure we're covering important test cases.

[jorisdral]

The PR is ready for a second review round. See the update Description of this PR for some info on the major changes that this PR makes.

• Note for reviewers: once Fix missing liblmdb-dev depency in CI #4214 is merged, I will rebase this branch on top of feature/utxo-hd

[dnadales]

We should decide which of the remaining TODOs in the code we should address.

[jasagredo]

I think it looks good, I do have some comments here and there

[ghost]

There's no 0.2.1 version of quickcheck-dynamic that's going to be released, the next version will be 3.0.0 because it's a breaking change from 2.0.0 which is the latest published on hackage.

[ghost]

Also, I am not too sure what quickcheck-lockstep adds on top of quickcheck-dynamic that could not be written simply using postcondition

[jorisdral]

There's no 0.2.1 version of quickcheck-dynamic that's going to be released, the next version will be 3.0.0 because it's a breaking change from 2.0.0 which is the latest published on hackage.

Thank you for pointing this out, I've amended this in the code and the corresponding GH issue

[edsko]

Also, I am not too sure what quickcheck-lockstep adds on top of quickcheck-dynamic that could not be written simply using postcondition

I don't really understand this sentiment. Sure, of course, technically speaking it's true that quickcheck-lockstep just "gives you a postcondition", but only in the same way that quickcheck-dynamic "just gives you a property". The quickcheck-dynamic library gives you event generation, shrinking, variable management, etc., but it gives you no infrastructure for determining if the responses from the system under test are correct or not. In order to know that, typically you need some kind of model; management of that model is what quickcheck-lockstep gives you. Of course, quickcheck-lockstep is less general than quickcheck-dynamic, advocating a specific style of testing; but for that style of testing, it keeps track of the model state, it gives you variable management for model responses (just like quickcheck-dynamic gives you variable management for the system under test), etc. It also gives you a more expressive variable, which support some kind of fmap-like structure. This is extremely useful when you have actions that can fail and therefore return something of type, say, Either Error a, but you want to refer to the result of such an action in later actions -- but not to any error results.

[ghost]

@edsko I was expressing my sentiment in the context of those tests, not in general. I failed to see the added value in this particular case because it seemed to me the checks could have been equally well, and perhaps more simply (ie. without an additional conceptual layer added), expressed with qc-d. I may be wrong of course.