No shrinking happening when checking a DL formula

[ghost]

I am surprised by the fact I don't see any trace of shrinking happening with some property I am checking, although I implemented shrinkAction. precondition = const True

Here is the DL property I am checking:

accept_all_non_conflicting_txs :: DL MempoolModel ()
accept_all_non_conflicting_txs = do
    anyActions_
    getModelStateDL >>= \case
        MempoolModel{transactions} ->
            eventually (HasValidatedTxs transactions)
        _ -> pure ()
  where
    eventually a = action (Wait 10) >> action a

and the resulting failure:

ouroboros-consensus
  Mempool
    Mempool Model
      eventually accepts all non-conflicting txs: FAIL
        *** Failed! Assertion failed (after 8 tests):
        DLScript
          [Do $ Var 0 := InitMempool (MempoolAndModelParams {immpInitialState = TestLedger {lastAppliedPoint = At (Block {blockPointSlot = SlotNo 14, blockPointHash = (testHashFromList [15,14,26,6,21,4])}), payloadDependentState = TestL
edgerState {availableTokens = fromList [Token {unToken = 4},Token {unToken = 5},Token {unToken = 7}]}}, immpLedgerConfig = EraParams {eraEpochSize = EpochSize 100, eraSlotLength = SlotLength 2s, eraSafeZone = StandardSafeZone 20}}),
           Do $ Var 1 := AddTxs [Tx {consumed = fromList [Token {unToken = 4},Token {unToken = 7}], produced = fromList [Token {unToken = 1},Token {unToken = 2},Token {unToken = 4},Token {unToken = 5},Token {unToken = 8}]}],
           Do $ Var 2 := AddTxs [Tx {consumed = fromList [Token {unToken = 4},Token {unToken = 5}], produced = fromList [Token {unToken = 5},Token {unToken = 6}]}],
           Do $ Var 3 := AddTxs [Tx {consumed = fromList [Token {unToken = 1},Token {unToken = 2},Token {unToken = 8}], produced = fromList [Token {unToken = 8}]}],
           Do $ Var 4 := AddTxs [Tx {consumed = fromList [Token {unToken = 5}], produced = fromList [Token {unToken = 0},Token {unToken = 1},Token {unToken = 3},Token {unToken = 4}]}],
           Do $ Var 5 := AddTxs [Tx {consumed = fromList [Token {unToken = 0},Token {unToken = 8}], produced = fromList [Token {unToken = 2}]}],
           Do $ Var 6 := AddTxs [Tx {consumed = fromList [Token {unToken = 1},Token {unToken = 4},Token {unToken = 6}], produced = fromList [Token {unToken = 2},Token {unToken = 3},Token {unToken = 4},Token {unToken = 8}]}],
           Do $ Var 7 := AddTxs [Tx {consumed = fromList [Token {unToken = 2}], produced = fromList [Token {unToken = 1},Token {unToken = 3},Token {unToken = 4},Token {unToken = 5}]}],
           Do $ Var 8 := Wait 10,
           Do $ Var 9 := HasValidatedTxs [Tx {consumed = fromList [Token {unToken = 4},Token {unToken = 7}], produced = fromList [Token {unToken = 1},Token {unToken = 2},Token {unToken = 4},Token {unToken = 5},Token {unToken = 8}]},Tx {
consumed = fromList [Token {unToken = 4},Token {unToken = 5}], produced = fromList [Token {unToken = 5},Token {unToken = 6}]},Tx {consumed = fromList [Token {unToken = 1},Token {unToken = 2},Token {unToken = 8}], produced = fromList [To
ken {unToken = 8}]},Tx {consumed = fromList [Token {unToken = 5}], produced = fromList [Token {unToken = 0},Token {unToken = 1},Token {unToken = 3},Token {unToken = 4}]},Tx {consumed = fromList [Token {unToken = 0},Token {unToken = 8}],
 produced = fromList [Token {unToken = 2}]},Tx {consumed = fromList [Token {unToken = 1},Token {unToken = 4},Token {unToken = 6}], produced = fromList [Token {unToken = 2},Token {unToken = 3},Token {unToken = 4},Token {unToken = 8}]},Tx
 {consumed = fromList [Token {unToken = 2}], produced = fromList [Token {unToken = 1},Token {unToken = 3},Token {unToken = 4},Token {unToken = 5}]}]]

I would expect this part *** Failed! Assertion failed (after 8 tests): to tell me it tried some shrinking.

I am using q-d v 2.0.0.

[MaximilianAlgehed]

Hm, this is a bit of a thorny one. We would certainly like to shrink this test case as the action calls happening after anyActions_ are entirely deterministic. What's happening (I think) is that q-d will happily remove stuff so long as the action parts of the trace still match precisely. The problem here is that your action mentions "too much" of the state - so the action in the counterexample can't be shrunk without becoming "desynched" with the action call in the DL property.

This is a bit of a problem here because fundamentally speaking I see no exact reason why this has to be the case. It's just a feature of how qc-d shrinks stuff. I guess we could try to change that so that if you remove actions from anyActions_ in a way that changes a later action you also change the result of that action in the shrunk trace...

I think the offending code is here:
https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs#L628

However, fixing this might require a serious rework of the shrinking implementation. But it might well be worth doing.

[ghost]

Thanks a lot for the clarification! I was puzzled because simply tracing the calls I could see shrinkAction to be ultimately called from forAllDL. Your explanation makes sense, if I rephrase it in my words, it means that shrinking traces generated by a DL formula still requires the shrunk trace to still match the DL formula but this is currently done in such a way that it's not really possible?

[ghost]

Actually, I was being stupid: I used forAllDL_ to run the formula which AFAICT does not shrink. Switching to forAllDL shows it actually tries to shrink.

[MaximilianAlgehed]

That's good! But we should still try to fix this behaviour! I have a minial failing example of this that showcases it nicely!

[MaximilianAlgehed]

Ok, we have a nice example of this now on branch issue-31. C.f. this module for an example of a property badProp that should always shrink to a minimal counterexample but doesn't:

λ> quickCheck badProp 
*** Failed! Assertion failed (after 4 tests):                   
do action $ Incr
   action $ Incr
   action $ Incr
   action $ Incr
   action $ Assert 4
   pure ()

λ> quickCheck badProp 
*** Failed! Assertion failed (after 4 tests):                   
do action $ Incr
   action $ Incr
   action $ Assert 2
   pure ()

The latter counterexample is minimal but because there is a tight coupling between the number of calls to Incr and the argument to Assert we can never shrink this property as quickcheck-dynamic will throw away any counterexamples that contain fewer calls to Incr than the argument to Assert.

[ghost]

I was wondering if we could not apply a strategy similar to Brozowski's Regular Languages derivatives, eg. compute a new expression by "deriving" it w.r.t. to some event it produces.

[MaximilianAlgehed]

That's actually what we currently do in shrinking in quite an ingenious way. The code currently shrinks counterexamples without reference to the DL formula and then checks that they are OK (and completes them) by taking the Brozowski derivative and doing the minimal work to complete the formula (the last bit is IIRC, or we just drop the ones that don't have derivative epsilon).

The problem with that is that if your action depends on the state and your old counterexample contains an action that depends on the state in the old counterexample then the derivative will fail. You can't derive the DL formula action A w.r.t. actual action B. This means that what we do want to do is actually say "yes I know it says action A and you have B so the thing I'm going to do is just change the counterexample to say A here". In a sense this is mixing taking the Brozowski derivative with doing the shrinking.

[ghost]

Ah, I did not realise that you were using this technique. I must admit the code is a bit dense for me :)
But contrary to regular language, here you need to do the derivation from the "end' right?

[MaximilianAlgehed]

I must admit the code is a bit dense for me too. I'm working on finding the time to go over it and re-work the whole thing. That's something for when I fix this bug...

[ghost]

I have updated related branch to main and tried to wrap my head around the problem. Ultimately, it hinges on the fact that traces depend on the state both at generation time and at shrinking time which seems to imply that we need to integrate both aspects in the same process in order to solve that problem.
Would it not help if we "reified" the dependency on the current state in the DL expressions, e.g if we explicit had a Decide node in the DL AST that would depend on the state?

[MaximilianAlgehed]

That might help materialize the dependency yes, the problem is that we have i <- counter <$> getModelStateDL; action $ Assert i for the following definition of getModelStateDL:

getModelStateDL :: DL s s
getModelStateDL = DL $ \s k -> k (underlyingState s) s

Changing this to materialize the fact that we are looking at the state at this point might help because that would mean we'd be shrinking not an action that uses the old state (from generation time) but one that uses the new state (in the continuation of the new Decide AST node).

In fact, I wonder if this can be used to entirely eliminate the Annotated s argument of DL - thus making the actual DynLogicFormula you're shrinking not relative to the model state at generation time?

[ghost]

I am experimenting with this, added a Decide (s -> ActionWithPolarity s a) (DynPred s) constructor to DynLogic but still struggling 😓

[MaximilianAlgehed]

Decide (Annotated s -> DynPred s)?

[ghost]

It looks like this in the DL:

dl = do
  anyActions_
  onState (Assert . counter)
  return ()

I am bit lost in the maze of continuations, and cannot convince the engine to properly "shrink" the Assert but will keep trying.

[MaximilianAlgehed]

The problem with that is that the continuation-in-monad approach is really cumbersome to work with and it doesn't buy you much. It also breaks a bunch of functionality you really need - like deciding what the rest of the DL property will look like depending on the state.

[MaximilianAlgehed]

With (Annotated s -> ActionWithPolarity s a) you can't change the DL property depending on the state. Even worse, you can't even run multiple actions to get to the appropriate state if need be.

[ghost]

Note that my Decide has both things: DynPred is reallyAnnotatedState s -> DynLogic s

[MaximilianAlgehed]

Right, my point is just that the first part shouldn't be necessary. Also whoever invented the DynPred thing should be given a stern talking to...

[ghost]

I felt the need to add this in order to be able to have a different action depending on the state, whereas in the After we have the action depending on the Var. It seems that's what we are after, aren't we?

[MaximilianAlgehed]

Not quite, the problem is that the action in the After is given a hard coded thing that was in the original state, not in the state you would have in the shrunk trace. Here you can execute the shrunk trace and materialise the getModelStateDL calls and importantly change what DL action is in the continuation.