Fix preconditions check

[AlexeyRaga]

Precondition and Require wasn't properly checked while shrinking

[moodmosaic]

LGTM! Left one comment/question.

[moodmosaic]

This skips actions that fail Precondition but continues with the previous state. Is that correct? Or should it filter them out entirely during generation? 🤔

[AlexeyRaga]

Yes, it is the intent.
We just skip actions whose precondition says "cannot execute in this state".
It is not only generation, but also shrinking that is at play... The intent is that when an action is removed from an already generated valid sequence (during shrinking), we still need to validate if the action still makes sense to execute.

This is what Haskell version does, too, and this is why Update in Haskell is polymorphic in kind (concrete, symbolic).

I am trying to simplify the story around calling Update a bit, not very successfully so far, but I am still hopeful :)

[moodmosaic]

I find fast-check's approach way more pragmatic:

A commands is defined for each one of the public functions of the SUT. They come with two methods:

• check(m: Readonly<Model>): boolean to allow or not allow the command to be executed given the current state.
• run(m: Model, r: Real): void to execute the command on the SUT and update the model accordingly.
  • Also checks for potential problems or inconsistencies between the model and the SUT.
• toString() used for shrinking/labeling

This doesn't even need a special library, it can be a shuffle of command-array objects! :)

---

I know it sounds "too simple" but using this simple model I've done large-scale, consensus-critical, model-based testing when I was at the Stacks Foundation for PoX-4 and SIP-031 boot (core, protocol, consensus) contracts.

[moodmosaic]

(See also: https://github.com/moodmosaic/counter-invariant-tests/blob/99c9987c446c74feb1acf970993214c7b2350b53/tests/counter/counter.invariant.test.ts#L14-L21)

[AlexeyRaga]

Yes, but the execution model there is fairly different from what Hedgehog does.
HH is two-stages: generation and execution. Plus automatic shrinking complicates things a lot.

For check we have Precondition and for run we have Execute. Which is the same.

But because HH has two stages: generation (with integrated shrinking trees, etc.) and execution, we have these two checks: symbolically first, and concrete later.

Here I am modeling against Haskell Hedgehog 🤷 and in my understanding the gen-time precondition is needed to only generate sequences that make sense before executing them.

I haven't checked, but fast-check probably cannot do it. It will probably interleave generation and execution, trying to generate next command?
Or will it generate invalid sequences to only realise it at the execution time?
This is not how HH works with its integrated shrinking 🤷‍♂️, different idea.

I guess that one can try building completely random sequences of actions and try executing them one-by-one while only checking at runtime for the validity of the next action...
Not sure how it matches HH idea (and implementation), but, again, here I am modeling after Haskell's HH Stateful.

[moodmosaic]

I really appreciate all the thought you're putting into this. Let me share some perspective that might be helpful.

I haven't done large-scale, consensus-critical, model-based testing with HH at the scale I've used fast-check's approach. I've used HH in projects, but not at that level. If you can point me to a codebase using HH's model-based testing at large scale, I'd love to see it and might be able to tell more. If you've personally used HH's model-based testing at large scale, that's more than enough validation!

But if you haven't (and are porting it here to use in .NET based on the design), I'd like to ask us to take a collective step back. I'm concerned we might be adding unnecessary complexity for no proven reason.

fast-check's approach is pragmatic and simple. fsharp-hedgehog doesn't necessarily need to replicate HH's approach 1:1 — we can take the best ideas from multiple ecosystems.

I've been using fast-check against PoX-4 (Proof of Transfer v4, the Stacks blockchain's consensus mechanism) and SIP-031 (Stacks Improvement Proposal for signer key rotation) when I was at Stacks Foundation. These are consensus-critical, production blockchain contracts. The efforts can be seen here:

• SIP-031 initial set of commands: https://github.com/stacks-network/stacks-core/pull/6321/changes#diff-adb5e0d70e3ba2936b90a93235b5d012948d51c1895868b418cb026277b95fb3
• All PoX-4 commands: https://github.com/stacks-network/stacks-core/tree/e6c240e0c0dc763b1cff8fd5fca7b4c237da8bdb/contrib/boot-contracts-stateful-prop-tests/tests/pox-4

I am not proposing or favoring JS/TS or fast-check over Haskell/Hedgehog/.NET/x/y/z. All I am saying is I'd rather port something I know works in practice and at scale, rather than porting something because "that's how it's done there in HH".

The two-stage generation/execution model with symbolic/concrete distinction adds real complexity. What concrete benefits does it provide that justify that complexity? Especially if we don't have evidence of it being battle-tested at scale?

[AlexeyRaga]

OK, no worries.
Since Hedgehog.Stateful is in beta stage, very deliberately, let's regroup and delete it from this repo.
We can think about another approach, and in a meantime nothing prevents me from having it as a personal package.
I am very interested implementing Hedgehog-like approach, but I can do it separately :)

I'm taking down this PR and will make another one removing Hedgehog.Stateful from here.

[AlexeyRaga]

As for reasoning: I value Hedgehog for its very efficient integrated shrinking.
I think that it is the main idea behind Hedgehog in the first place, and if not that, then I could use any other framework, like FSCheck or said fast-check.

I believe that it is possible to implement fast-check way on top of Hedgehog.FSharp, but I cannot see how efficient shrinking can be preserved under that model.
Not that I want complicated API per se, it is a trade-off to keep this big idea working consistently instead of saying "oh, in this corner of Hedgehog we give up and make a different choice".

I mean, shrinking can still be done, but much, much less efficiently.
I'll be happy to stand corrected on this though! :)

In my line of work (testing APIs) efficient shrinking is important: it is network, time and load on SUT that matters, this is why Hedgehog idea of efficient integrated shrinking motivates me :)