Difference between forAllQ and forAllNonVariableQ?

[ch1bo]

Is shrinking different? What is the difference?

Maybe this is also a bug report on shrinking behavior.

We are sometimes generating actions in DL like this:

  -- seed world
  forAllQ (withGenQ genSeed (const [])) >>= action_
  -- init head
  WorldState{hydraParties} <- getModelStateDL
  forAllQ (withGenQ (genInit hydraParties) (const [])) >>= action_

which when failing, shrinks in a way it invalidates a pre-condition, e.g.

Falsified (after 1 test and 1 shrink):
         do _ <- forAllQ $ exactlyQ $ Init (Party {vkey = HydraVerificationKey (VerKeyEd25519DSIGN "55517edd313790d7ac8140e12c783847fad49f9f7b242d385423db7b9ff2443d")})
            -- In state: [] |- WorldState {hydraParties = [], hydraState = Start}
            action $ Init (Party {vkey = HydraVerificationKey (VerKeyEd25519DSIGN "55517edd313790d7ac8140e12c783847fad49f9f7b242d385423db7b9ff2443d")})  -- Failed precondition
            pure ()

(If I run this with max shrinks 0 it shows the actually failing model / perform).

However, when exchanging the first forAllQ with forAllNonVariableQ this does not fail on precondition when shrinking (supposedly, given the test output saying "1 test and 1 shrink").

[MaximilianAlgehed]

For forAllQ you have to supply a quantification over a type that satisfies type QuantifyConstraints a = (Eq a, Show a, Typeable a, HasVariables a). However, if you know there are no symbolic variables in the type you're quantifying over you can use forAllNonVariableQ to get around having to write a HasVariables instance. However, this is generally unsafe if the type you're quantifying over does have variables.

Now, as for the behaviour above assuming we see everything that's in the Init constructor I'm a bit perplexed - because there are no variables here. If there was a variable in the value in the exactlyQ that would indeed cause a precondition failure because that would not be allowed in the empty variable context (the [] |- part of the In state: comment).

Could you please provide some more details including the definition of the action type and the precondition, a small original failing trace, and the failing trace?

Moreover, I thought we removed withGenQ because it is unsafe! @abailly ??

Yeah, I was about to suggest the problem might lie in the use of withGenQ, checkout #65

[MaximilianAlgehed]

As for why this is different with forAllQ vs forAllNonVariableQ thinking more about it I think that's just the issue with withGenQ.

@ch1bo I am not sure if this is the case, but the problem might be similar: withGenQ does not "filter" generated values when it shrinks, even though it should because it might be the case such a value becomes invalid. This is a problem I stumbled upon in the conflict-free liveness property and then I "fixed" by explicitly constructing a quantification that handles filter

[MaximilianAlgehed]

The "correct" way of doing this in DL is to rewrite the genSeed and genInit generators as DL state () things that use safe Quantifications to build the actions and then puts them together.

However, the issue I'm seeing here is that the action_ call from the first line is shrunk away in the counterexample. That I find very strange - explicit calls to action shouldn't be removed during shrinking.

[MaximilianAlgehed]

@abailly-iohk 's analysis of the problem with withGenQ is correct. However, I still struggle with the action being shrunk away. That I find worrying.

[MaximilianAlgehed]

@ch1bo could you please put the whole test and test output here so I can have a look. Because something is fishy here.

[ch1bo]

@MaximilianAlgehed We moved on and our code is a mess, but you might be able to use the following to reproduce this:

• Checkout cardano-scaling/hydra@8b157e5
• cabal test hydra-node --test-options '-m "Model/check head opens"' should give you this output:

Build profile: -w ghc-9.6.4 -O1
In order, the following will be built (use -v for more details):
 - hydra-node-0.15.0 (test:tests) (first run)
Preprocessing test suite 'tests' for hydra-node-0.15.0..
Building test suite 'tests' for hydra-node-0.15.0..
Running 1 test suites...
Test suite tests: RUNNING...

Hydra.Model
  check head opens if all participants commit FAILED [1]

Failures:

  test/Hydra/ModelSpec.hs:184:3: 
  1) Hydra.Model check head opens if all participants commit
       Falsified (after 1 test and 1 shrink):
         do _ <- forAllQ $ exactlyQ $ Init (Party {vkey = HydraVerificationKey (VerKeyEd25519DSIGN "74e3f748f8bc794eb2d91b05c0c4babfa9e0042b09568390c8aba89a2292e1ba")})
            -- In state: [] |- WorldState {hydraParties = [], hydraState = Start}
            action $ Init (Party {vkey = HydraVerificationKey (VerKeyEd25519DSIGN "74e3f748f8bc794eb2d91b05c0c4babfa9e0042b09568390c8aba89a2292e1ba")})  -- Failed precondition
            pure ()

  To rerun use: --match "/Hydra.Model/check head opens if all participants commit/"

Randomized with seed 1700275801

Finished in 0.0589 seconds
1 example, 1 failure
Test suite tests: FAIL
Test suite logged to:
/home/ch1bo/code/iog/hydra/dist-newstyle/build/x86_64-linux/ghc-9.6.4/hydra-node-0.15.0/t/tests/test/hydra-node-0.15.0-tests.log
0 of 1 test suites (0 of 1 test cases) passed.

• Then this commit (one ahead of thee above) should make the same test fail on the non-shrinked actions cardano-scaling/hydra@052a16c