Do not verify lengths in propWithModel

The input length is not always equal to the output length, nor even
predictable. Furthermore, some properties might not be interested in the
length in the first place.

Fixes #81

clash-protocols.cabal

@@ -135,7 +135,8 @@ library
 
   build-depends:
       -- inline-circuit-notation
-      circuit-notation
+    , circuit-notation
+    , clash-prelude-hedgehog
     , data-default
     , deepseq
     , extra

src/Protocols/Avalon/Stream.hs

@@ -251,9 +251,8 @@ instance
   ) =>
   Test (AvalonStream dom conf dataType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options
       $ Df.maybeToData
       <$> sampled
 

src/Protocols/Axi4/Stream.hs

@@ -17,7 +17,6 @@ import Control.DeepSeq (NFData)
 import Data.Hashable (Hashable, hashWithSalt)
 import qualified Data.Maybe as Maybe
 import Data.Proxy
-import qualified Prelude as P
 
 -- clash-prelude
 import Clash.Prelude hiding (concat, length, take)
@@ -129,7 +128,7 @@ instance
     s0 = ()
     blankOtp = Nothing
     stateFn ack _ otpItem =
-      pure (otpItem, Nothing, Maybe.isJust otpItem && _tready ack)
+      pure (otpItem, Nothing, Maybe.isJust otpItem C.&& _tready ack)
 
   fromDfCircuit proxy = DfConv.fromDfCircuitHelper proxy s0 blankOtp stateFn
    where
@@ -153,7 +152,7 @@ instance
   sigToSimFwd _ s = sample_lazy s
   sigToSimBwd _ s = sample_lazy s
 
-  stallC conf (head -> (stallAck, stalls)) =
+  stallC conf (C.head -> (stallAck, stalls)) =
     withClockResetEnable clockGen resetGen enableGen
       $ DfConv.stall Proxy Proxy conf stallAck stalls
 
@@ -187,9 +186,8 @@ instance
   ) =>
   Test (Axi4Stream dom conf userType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options
       $ Df.maybeToData
       <$> sampled
 

src/Protocols/Hedgehog.hs

@@ -41,8 +41,10 @@ import Protocols.Hedgehog.Internal
 -- clash-prelude
 import qualified Clash.Prelude as C
 
--- hedgehog
+-- clash-prelude-hedgehog
+import Clash.Hedgehog.Sized.Vector (genVec)
 
+-- hedgehog
 import Hedgehog ((===))
 import qualified Hedgehog as H
 import qualified Hedgehog.Gen as Gen
@@ -60,6 +62,15 @@ resetGen n =
   C.unsafeFromActiveHigh
     (C.fromList (replicate n True <> repeat False))
 
+smallInt :: H.Range Int
+smallInt = Range.linear 0 10
+
+genSmallInt :: H.Gen Int
+genSmallInt = Gen.frequency
+  [ (90, Gen.integral smallInt)
+  , (10, Gen.constant (Range.lowerBound 99 smallInt))
+  ]
+
 {- | Test a protocol against a pure model implementation. Circuit under test will
 be arbitrarily stalled on the left hand and right hand side and tested for
 a number of properties:
@@ -89,21 +100,23 @@ propWithModel ::
   H.Property
 propWithModel eOpts genData model prot prop = H.property $ do
   dat <- H.forAll genData
-  let n = maximum (expectToLengths (Proxy @a) dat)
+
+  -- TODO: Different 'n's for each output
+  n <- H.forAll (Gen.integral (Range.linear 0 (eoSampleMax eOpts)))
 
   -- TODO: Different distributions?
-  let genStall = Gen.integral (Range.linear 0 10)
+  let genStall = genSmallInt
 
   -- Generate stalls for LHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode))
+  lhsStallModes <- H.forAll (genVec genStallMode)
   lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes)
 
   -- Generate stalls for RHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode))
+  rhsStallModes <- H.forAll (genVec genStallMode)
   rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes)
 
   let
@@ -121,10 +134,9 @@ propWithModel eOpts genData model prot prop = H.property $ do
         |> prot
         |> rhsStallC
     sampled = sampleC simConfig stalledProtocol
-    lengths = expectToLengths (Proxy @b) expected
 
   -- expectN errors if circuit does not produce enough data
-  trimmed <- expectN (Proxy @b) eOpts lengths sampled
+  trimmed <- expectN (Proxy @b) eOpts sampled
 
   _ <- H.evalNF trimmed
   _ <- H.evalNF expected

src/Protocols/Hedgehog/Internal.hs

@@ -11,11 +11,8 @@ Internals for "Protocols.Hedgehog".
 module Protocols.Hedgehog.Internal where
 
 -- base
-
-import Control.Monad (forM)
-import Data.Maybe (fromMaybe)
 import Data.Proxy (Proxy (Proxy))
-import GHC.Stack (HasCallStack, withFrozenCallStack)
+import GHC.Stack (HasCallStack)
 import Prelude
 
 -- clash-protocols
@@ -33,17 +30,17 @@ import Control.DeepSeq
 -- hedgehog
 import qualified Hedgehog as H
 import qualified Hedgehog.Internal.Property as H
-import qualified Hedgehog.Internal.Show as H
-
--- pretty-show
-import Text.Show.Pretty (ppShow)
 
 -- | Options for 'expectN' function. See individual fields for more information.
 data ExpectOptions = ExpectOptions
-  { eoEmptyTail :: Int
-  -- ^ Sample /n/ cycles after last expected value and check for emptiness
-  , eoTimeout :: Maybe Int
-  -- ^ Timeout after seeing /n/ empty cycles
+  { eoStopAfterEmpty :: Int
+  -- ^ Stop sampling after seeing /n/ consecutive empty samples
+  , eoSampleMax :: Int
+  -- ^ Produce an error if the circuit produces more than /n/ valid samples. This
+  -- is used to prevent infinitely running circuits.
+  --
+  -- This number is used to generate stall information, so setting it to
+  -- unreasonable values will result in long runtimes.
   , eoResetCycles :: Int
   -- ^ Ignore first /n/ cycles
   , eoDriveEarly :: Bool
@@ -58,8 +55,13 @@ empty cycles.
 defExpectOptions :: ExpectOptions
 defExpectOptions =
   ExpectOptions
-    { eoEmptyTail = 50
-    , eoTimeout = Just 1000
+    -- XXX: These numbers are arbitrary, and should be adjusted to fit the
+    --      protocol being tested. Annoyingly, upping these values will
+    --      increase the time it takes to run the tests. This is because
+    --      the test will run for at least the number of cycles specified
+    --      in 'eoStopAfterEmpty'.
+    { eoStopAfterEmpty = 256
+    , eoSampleMax = 128
     , eoResetCycles = 30
     , eoDriveEarly = True
     }
@@ -81,22 +83,13 @@ class
   ) =>
   Test a
   where
-  -- | Get the number of expected valid data cycles for each data channel,
-  -- given a list of expected data.
-  expectToLengths ::
-    Proxy a ->
-    ExpectType a ->
-    C.Vec (SimulateChannels a) Int
-
   -- | Trim each channel to the lengths given as the third argument. See
   -- result documentation for failure modes.
   expectN ::
     (HasCallStack, H.MonadTest m) =>
     Proxy a ->
     -- | Options, see 'ExpectOptions'
     ExpectOptions ->
-    -- | Number of valid data cycles expected on each channel
-    C.Vec (SimulateChannels a) Int ->
     -- | Raw sampled data
     SimulateFwdType a ->
     -- | Depending on "ExpectOptions", fails the test if:
@@ -113,58 +106,29 @@ class
     m (ExpectType a)
 
 instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where
-  expectToLengths Proxy = pure . length
-
   expectN ::
     forall m.
     (HasCallStack, H.MonadTest m) =>
     Proxy (Df dom a) ->
     ExpectOptions ->
-    C.Vec 1 Int ->
     [Df.Data a] ->
     m [a]
-  expectN Proxy (ExpectOptions{eoEmptyTail, eoTimeout}) (C.head -> nExpected) sampled = do
-    go (fromMaybe maxBound eoTimeout) nExpected sampled
+  expectN Proxy (ExpectOptions{eoSampleMax, eoStopAfterEmpty}) sampled = do
+    go eoSampleMax eoStopAfterEmpty sampled
    where
-    catDatas [] = []
-    catDatas (Df.NoData : xs) = catDatas xs
-    catDatas (Df.Data x : xs) = x : catDatas xs
-
-    go ::
-      (HasCallStack) =>
-      -- Timeout counter. If it reaches zero we time out.
-      Int ->
-      -- Expected number of values
-      Int ->
-      -- Sampled data
-      [Df.Data a] ->
-      -- Results
-      m [a]
+    go :: (HasCallStack) => Int -> Int -> [Df.Data a] -> m [a]
     go _timeout _n [] =
       -- This really should not happen, protocols should produce data indefinitely
       error "unexpected end of signal"
-    go _timeout 0 rest = do
-      -- Check for superfluous output from protocol
-      case catDatas (take eoEmptyTail rest) of
-        [] -> pure (take nExpected (catDatas sampled))
-        superfluous ->
-          let err = "Circuit produced more output than expected:"
-           in H.failWith Nothing (err <> "\n\n" <> ppShow superfluous)
-    go timeout n _
-      | timeout <= 0 =
-          H.failWith Nothing $
-            concat
-              [ "Circuit did not produce enough output. Expected "
-              , show n
-              , " more values. Sampled only " <> show (nExpected - n) <> ":\n\n"
-              , ppShow (take (nExpected - n) (catDatas sampled))
-              ]
-    go timeout n (Df.NoData : as) = do
-      -- Circuit did not output valid cycle, just continue
-      go (pred timeout) n as
-    go _ n (Df.Data _ : as) =
-      -- Circuit produced a valid cycle, reset timeout
-      go (fromMaybe maxBound eoTimeout) (pred n) as
+    go 0 _ _ =
+      H.failWith Nothing ("Sample limit reached after sampling " <> show eoSampleMax <> " samples")
+    go _ 0 _ =
+      pure []
+    go sampleTimeout _emptyTimeout (Df.Data a : as) =
+      (a:) <$> go (sampleTimeout - 1) eoStopAfterEmpty as
+    go sampleTimeout emptyTimeout (Df.NoData : as) =
+      go sampleTimeout (emptyTimeout - 1) as
+
 
 instance
   ( Test a
@@ -174,27 +138,16 @@ instance
   ) =>
   Test (C.Vec n a)
   where
-  expectToLengths ::
-    Proxy (C.Vec n a) ->
-    ExpectType (C.Vec n a) ->
-    C.Vec (n * SimulateChannels a) Int
-  expectToLengths Proxy =
-    C.concatMap (expectToLengths (Proxy @a))
-
   expectN ::
     forall m.
     (HasCallStack, H.MonadTest m) =>
     Proxy (C.Vec n a) ->
     ExpectOptions ->
-    C.Vec (n * SimulateChannels a) Int ->
     C.Vec n (SimulateFwdType a) ->
     m (C.Vec n (ExpectType a))
-  expectN Proxy opts nExpecteds sampled = do
-    -- TODO: This creates some pretty terrible error messages, as one
-    -- TODO: simulate channel is checked at a time.
-    forM
-      (C.zip (C.unconcatI nExpecteds) sampled)
-      (uncurry (expectN (Proxy @a) opts))
+  -- TODO: This creates some pretty terrible error messages, as one
+  -- TODO: simulate channel is checked at a time.
+  expectN Proxy opts = mapM (expectN (Proxy @a) opts)
 
 instance
   ( Test a
@@ -203,59 +156,16 @@ instance
   ) =>
   Test (a, b)
   where
-  expectToLengths ::
-    Proxy (a, b) ->
-    (ExpectType a, ExpectType b) ->
-    C.Vec (SimulateChannels a + SimulateChannels b) Int
-  expectToLengths Proxy (t1, t2) =
-    expectToLengths (Proxy @a) t1 C.++ expectToLengths (Proxy @b) t2
-
   expectN ::
     forall m.
     (HasCallStack, H.MonadTest m) =>
     Proxy (a, b) ->
     ExpectOptions ->
-    C.Vec (SimulateChannels a + SimulateChannels b) Int ->
     (SimulateFwdType a, SimulateFwdType b) ->
     m (ExpectType a, ExpectType b)
-  expectN Proxy opts nExpecteds (sampledA, sampledB) = do
+  expectN Proxy opts (sampledA, sampledB) = do
     -- TODO: This creates some pretty terrible error messages, as one
     -- TODO: simulate channel is checked at a time.
-    trimmedA <- expectN (Proxy @a) opts nExpectedsA sampledA
-    trimmedB <- expectN (Proxy @b) opts nExpectedsB sampledB
+    trimmedA <- expectN (Proxy @a) opts sampledA
+    trimmedB <- expectN (Proxy @b) opts sampledB
     pure (trimmedA, trimmedB)
-   where
-    (nExpectedsA, nExpectedsB) = C.splitAtI nExpecteds
-
--- | Fails with an error that shows the difference between two values.
-failDiffWith ::
-  (H.MonadTest m, Show a, Show b, HasCallStack) =>
-  -- | Additional info for error message
-  String ->
-  -- | Expected
-  a ->
-  -- | Actual
-  b ->
-  m ()
-failDiffWith msg x y =
-  case H.valueDiff <$> H.mkValue x <*> H.mkValue y of
-    Nothing ->
-      withFrozenCallStack $
-        H.failWith Nothing $
-          unlines $
-            [ msg
-            , "━━ expected ━━"
-            , H.showPretty x
-            , "━━ actual ━━"
-            , H.showPretty y
-            ]
-    Just vdiff@(H.ValueSame _) ->
-      withFrozenCallStack $
-        H.failWith
-          (Just $ H.Diff "━━━ Failed (" "" "no differences" "" ") ━━━" vdiff)
-          msg
-    Just vdiff ->
-      withFrozenCallStack $
-        H.failWith
-          (Just $ H.Diff "━━━ Failed (" "- expected" ") (" "+ actual" ") ━━━" vdiff)
-          msg

src/Protocols/Wishbone/Standard/Hedgehog.hs

@@ -480,7 +480,7 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do
     resets = 5
     driver = driveStandard @dom (defExpectOptions{eoResetCycles = resets}) (P.zip input reqStalls)
     circuit1 = validatorCircuit |> circuit0
-    (_, s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1
+    (_, s2m) = observeComposedWishboneCircuit (eoSampleMax eOpts) driver circuit1
 
   matchModel 0 s2m input st === Right ()
  where
@@ -504,17 +504,13 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do
 
 observeComposedWishboneCircuit ::
   (KnownDomain dom) =>
-  Maybe Int ->
+  Int ->
   Circuit () (Wishbone dom mode addressWidth a) ->
   Circuit (Wishbone dom mode addressWidth a) () ->
   ( [WishboneM2S addressWidth (BitSize a `DivRU` 8) a]
   , [WishboneS2M a]
   )
-observeComposedWishboneCircuit Nothing (Circuit master) (Circuit slave) =
-  let ~((), m2s) = master ((), s2m)
-      ~(s2m, ()) = slave (m2s, ())
-   in (sample_lazy m2s, sample_lazy s2m)
-observeComposedWishboneCircuit (Just n) (Circuit master) (Circuit slave) =
+observeComposedWishboneCircuit n (Circuit master) (Circuit slave) =
   let ~((), m2s) = master ((), s2m)
       ~(s2m, ()) = slave (m2s, ())
    in (sampleN_lazy n m2s, sampleN_lazy n s2m)