packages feed

hedgehog-lockstep (empty) → 0.1.0.0

raw patch · 24 files changed

+3461/−0 lines, 24 filesdep +barbiesdep +basedep +containers

Dependencies added: barbies, base, containers, hedgehog, hedgehog-lockstep, mtl

Files

+ CHANGELOG.md view
@@ -0,0 +1,92 @@+# Changelog++All notable changes to `hedgehog-lockstep` will be documented in this file.++The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),+and this project adheres to [Haskell PVP](https://pvp.haskell.org/).++## 0.1.0.0++Initial release.++### Added++- `LockstepCmd` record bundling an API operation with its model+  interpretation and observation.+- `LockstepState` wrapping a user-defined model plus a `ModelEnv`,+  a `Map` keyed by Hedgehog `Var` identity (O(log n) lookup) using a+  phase-polymorphic `Ord1`-based comparison. `initialLockstepState`,+  `getModel`, and `getEntries` construct and project from it.+- `GVar` and `Op` (`OpId`, `OpFst`, `OpSnd`, `OpLeft`, `OpRight`,+  `OpComp`, plus `(>>>)` for left-to-right composition) for projecting+  values out of compound action outputs.+- `varsOfType`, `mkGVar`, `mkGVarId`, `mapGVar`, `resolveGVar`,+  `concreteGVar`, `gvarLabel` for enumerating and resolving generalized+  variables. `mapGVar` composes an additional projection (any+  `InterpretOp` instance, including the built-in `Op`) onto an existing+  `GVar`, the analogue of `quickcheck-lockstep`'s `mapGVar`.+- Four test entry points:+  `lockstepProperty`, `lockstepPropertyWith`, `lockstepParallel`, and+  `lockstepParallelWith`.+- Monad-parameterized variants+  `lockstepPropertyM`, `lockstepPropertyWithM`, `lockstepParallelM`, and+  `lockstepParallelWithM` accepting a+  `forall a. m a -> PropertyT IO a` (or `env -> m a -> PropertyT IO a`)+  natural transformation. Lets users write commands in a custom monad+  stack (e.g., `ReaderT env (PropertyT IO)`) and supply the runner+  separately, without hardcoding `PropertyT IO` into every `lsCmdExec`.+- `hoistLockstepCmd :: (forall a. m a -> n a) -> LockstepCmd m model -> LockstepCmd n model`+  for retargeting a command's monad.+- New module `Hedgehog.Lockstep.Observe` exposing an `Observation`+  GADT (`ObserveEq`, `ObserveProject`, `ObservePair`, `ObserveCustom`)+  and `runObservation`. The GADT factors out the common+  model-output-versus-real-output comparison patterns into a typed DSL+  so users can write `lsCmdObserve = runObservation ObserveEq` or+  `lsCmdObserve = runObservation (ObserveProject normM normR)` instead+  of writing the assertion by hand. This is the hedgehog-lockstep+  analogue of `quickcheck-lockstep`'s `Observable`/`ModelValue` split.+- New module `Hedgehog.Lockstep.Examples` exposing+  `lockstepLabelledExamples`, a model-only driver that samples random+  command sequences, accumulates the tags emitted by `lsCmdTag`, and+  prints one shortest sampled trace per tag. This is the analogue of+  `QuickCheck`'s `labelledExamples` and `quickcheck-lockstep`'s+  `tagActions`: it answers "is the generator actually hitting the+  labelled cases I expect" without running the real system at all.+  The accompanying `LabelledExamples` summary type and `ModelStep`+  trace entry are exposed for callers that want to inspect the+  sampled traces directly.+- `lockstepCommands` for users who want to drive+  `Gen.sequential` / `executeSequential` directly.+- README guidance and a `Test.KVStore` example for using+  `Hedgehog.label` / `classify` inside `lsCmdObserve` for coverage labels.+- `lsCmdInvariants :: model -> output -> Test ()` field on `LockstepCmd`+  for system invariants that should hold after every command, separate+  from the lockstep equality check in `lsCmdObserve`.+- `lsCmdTag :: model -> model -> modelOutput -> [String]` field on+  `LockstepCmd` for per-step coverage tagging. Receives the pre- and+  post-step model and the model's predicted output; each returned tag is+  reported via `Hedgehog.label`. This is the analogue of+  `quickcheck-lockstep`'s `tagStep` and is the natural place for tags+  whose value depends on how the model state changed during the step.+- Per-step model-state footnote: `toLockstepCommand` adds a `footnote`+  of the post-step model after every command. Hedgehog only displays+  footnotes on test failure, so passing tests are unaffected; on+  failure the model-state evolution shows alongside the shrunken+  command sequence (analogue of `quickcheck-lockstep`'s `monitoring`+  counterexample enrichment).+- Module-level Haddock for every public module, plus disambiguated+  identifier references so Haddock builds cleanly with no warnings.+- README caveat documenting the dependency on `Hedgehog.Internal.State`.+- `Test.UnitCoverage` exercising `applyOp`, `gvarLabel`, `mapGVar`, and+  `mkGVarId`.+- `InterpretOp` class with `interpretOp :: op a b -> a -> Maybe b`.+  `mkGVar` and `mapGVar` accept any op type with `InterpretOp` and+  `Show` instances, not just the built-in `Op`. Users can extend the+  projection vocabulary (e.g., a list-head op) by defining their own+  GADT and supplying instances. The built-in `Op` is itself an+  instance of `InterpretOp`, and `applyOp` is exported as a synonym+  for `interpretOp`. This is the analogue of `quickcheck-lockstep`'s+  `Operation`/`InterpretOp` classes, closing the structural-flexibility+  gap with that library.+- `Test.CustomOp` exercising a user-defined op (`MyOpHead :: MyOp [a] a`)+  end-to-end through a real lockstep test.
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2026, Josh Burgess++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice,+   this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+   this list of conditions and the following disclaimer in the documentation+   and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its+   contributors may be used to endorse or promote products derived from this+   software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,379 @@+# hedgehog-lockstep++Lockstep-style stateful property testing for [Hedgehog](https://hedgehog.qa/).++This library ports the ideas from [quickcheck-lockstep](https://github.com/well-typed/quickcheck-lockstep) onto Hedgehog's `Command`-based state machine framework, giving you:++- **Integrated shrinking** (no manual `shrinkWithVars`)+- **Parallel testing** via Hedgehog's `executeParallel`+- **Less boilerplate** than the quickcheck-lockstep / quickcheck-dynamic / QuickCheck stack+- **GVar projections** for referencing components of previous action outputs++## How it works++Write a pure **model** of your stateful system. Define **commands** that pair a real operation with its model interpretation. The library generates random command sequences, executes them against both the model and the real system, and checks that results agree at every step.++If they disagree, Hedgehog's integrated shrinking finds a minimal counterexample automatically.++## Quick example++Test a mutable key-value store against a pure `Map`:++```haskell+-- Model is a pure Map+type Model = Map String Int++-- Define inputs as barbies-style HKD types+data PutInput v = PutInput !String !Int deriving (Show)+instance FunctorB PutInput where bmap _ (PutInput k v) = PutInput k v+instance TraversableB PutInput where btraverse _ (PutInput k v) = pure (PutInput k v)++data GetInput v = GetInput !String deriving (Show)+instance FunctorB GetInput where bmap _ (GetInput k) = GetInput k+instance TraversableB GetInput where btraverse _ (GetInput k) = pure (GetInput k)++-- Define commands+cmdPut :: IORef (Map String Int) -> LockstepCmd (PropertyT IO) Model+cmdPut store = LockstepCmd+  { lsCmdGen        = \_ -> Just $ PutInput <$> Gen.element ["a","b","c"] <*> Gen.int (Range.linear 0 100)+  , lsCmdExec       = \(PutInput k v) -> evalIO $ modifyIORef' store (Map.insert k v) >> pure ()+  , lsCmdModel      = \st (PutInput k v) -> ((), Map.insert k v (getModel st))+  , lsCmdRequire    = \_ _ -> True+  , lsCmdObserve    = \() () -> pure ()+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++cmdGet :: IORef (Map String Int) -> LockstepCmd (PropertyT IO) Model+cmdGet store = LockstepCmd+  { lsCmdGen        = \_ -> Just $ GetInput <$> Gen.element ["a","b","c"]+  , lsCmdExec       = \(GetInput k) -> evalIO $ Map.lookup k <$> readIORef store+  , lsCmdModel      = \st (GetInput k) -> (Map.lookup k (getModel st), getModel st)+  , lsCmdRequire    = \_ _ -> True+  , lsCmdObserve    = \expected actual -> expected === actual+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++-- Run the property+prop_kvStore :: Property+prop_kvStore =+  lockstepPropertyWith+    Map.empty           -- initial model+    50                  -- max actions per test+    (newIORef Map.empty)           -- create resource+    (\ref -> writeIORef ref Map.empty)  -- reset before execution+    (\ref -> [cmdPut ref, cmdGet ref])  -- commands+```++## GVar: referencing previous outputs++When a command returns a compound type (e.g., `Either String (Handle, FilePath)`), later commands may need to reference a component of that result. `GVar` with `Op` projections handles this:++```haskell+-- Open returns Either String (Handle, Name)+-- Write needs the Handle, projected via OpRight >>> OpFst++data WriteInput v = WriteInput !(GVar Handle v) !String deriving (Show)++instance FunctorB WriteInput where+  bmap f (WriteInput gv s) = WriteInput (bmap f gv) s+instance TraversableB WriteInput where+  btraverse f (WriteInput gv s) = (\gv' -> WriteInput gv' s) <$> btraverse f gv++cmdWrite ref = LockstepCmd+  { lsCmdGen = \st ->+      case varsOfType @OpenResult st of+        [] -> Nothing+        vars -> Just $ do+          var <- Gen.element vars+          let op :: Op OpenResult Handle+              op = OpRight >>> OpFst+          content <- Gen.string (Range.linear 0 20) Gen.alpha+          pure $ WriteInput (mkGVar var op) content++  , lsCmdExec = \(WriteInput gv content) ->+      case concreteGVar gv of+        Just h  -> evalIO $ write ref h content+        Nothing -> pure (Left "bad handle")++  , lsCmdModel = \st (WriteInput gv content) ->+      case resolveGVar gv (getEntries st) of+        Just h  -> modelWrite (getModel st) h content+        Nothing -> (Left "bad handle", getModel st)+  , ...+  }+```++## Available Op projections++| Op | Projects from | To |+|----|--------------|-----|+| `OpId` | `a` | `a` |+| `OpFst` | `(a, b)` | `a` |+| `OpSnd` | `(a, b)` | `b` |+| `OpLeft` | `Either a b` | `a` (partial) |+| `OpRight` | `Either a b` | `b` (partial) |+| `OpComp f g` | composition | `g` then `f` |+| `f >>> g` | left-to-right | `f` then `g` |++Partial projections (`OpLeft`, `OpRight`) return `Nothing` on mismatch.++If you already hold a `GVar` and want to project further, use `mapGVar`:++```haskell+gv     :: GVar (Either err (Handle, Name)) v+gvHandle = mapGVar (OpRight >>> OpFst) gv  -- :: GVar Handle v+```++### Custom projections++The built-in `Op` covers pair, sum, identity, and composition. If you need+a projection it doesn't have (list head, record fields, custom decoders),+define your own GADT and write an `InterpretOp` instance plus a `Show`+instance. `mkGVar` and `mapGVar` accept any op that satisfies those+constraints:++```haskell+data MyOp a b where+  MyOfOp   :: Op a b -> MyOp a b   -- embed the built-ins+  MyOpHead :: MyOp [a] a           -- new: list head++instance InterpretOp MyOp where+  interpretOp (MyOfOp op) x       = interpretOp op x+  interpretOp MyOpHead    []      = Nothing+  interpretOp MyOpHead    (x : _) = Just x++instance Show (MyOp a b) where+  show (MyOfOp op) = show op+  show MyOpHead    = "head"++-- now usable anywhere a built-in Op was:+gvHead :: Var [Int] v -> GVar Int v+gvHead var = mkGVar var (MyOpHead :: MyOp [Int] Int)+```++`mkGVar` and `mapGVar` carry `Typeable` (and `Ord` on the real-side type)+constraints inherited from the underlying `Var`; in the example above+`[Int]` and `Int` satisfy them automatically. If you generalise the+element type you'll need to propagate the same constraints.++The library uses the `InterpretOp` instance to apply the projection during+both model and real resolution; the `Show` instance feeds the `gvarLabel`+chain shown in failure messages. See `test/Test/CustomOp.hs` for a full+end-to-end example.++## Structured observations++Plain `lsCmdObserve = \m r -> m === r` only works when the model output and the real output have the same type. Real APIs often violate that: a real `open` returns a `Handle` while the model returns an index; the real call returns a verbose error string while the model returns an abstract tag; both sides return rich records but only a subset of fields should be compared.++`Observation modelOutput output` is a small typed DSL that captures the common patterns:++```haskell+data Observation modelOutput output where+  ObserveEq      :: (Eq output, Show output) => Observation output output+  ObserveProject :: (Eq obs, Show obs)+                 => (modelOutput -> obs)+                 -> (output -> obs)+                 -> Observation modelOutput output+  ObservePair    :: Observation m1 o1+                 -> Observation m2 o2+                 -> Observation (m1, m2) (o1, o2)+  ObserveCustom  :: (modelOutput -> output -> Test ())+                 -> Observation modelOutput output++runObservation :: Observation modelOutput output -> modelOutput -> output -> Test ()+```++`runObservation` produces a function of exactly the shape `lsCmdObserve` expects, so:++```haskell+-- Same type on both sides:+lsCmdObserve = runObservation ObserveEq++-- Project both sides through a normaliser:+lsCmdObserve = runObservation (ObserveProject normaliseModel normaliseReal)++-- Tuple of independent observations:+lsCmdObserve = runObservation (ObservePair ObserveEq (ObserveProject id realToModel))++-- Escape hatch (equivalent to writing it inline):+lsCmdObserve = runObservation (ObserveCustom $ \m r -> ...)+```++This is the analogue of `quickcheck-lockstep`'s `Observable`/`ModelValue` GADT split, but lighter: you can mix structured observations with `lsCmdObserve = \m r -> ...` freely, file by file. See `test/Test/Observation.hs` for an example using `ObservePair` + `ObserveProject`.++## LockstepCmd fields++| Field | Type | Purpose |+|-------|------|---------|+| `lsCmdGen` | `LockstepState model Symbolic -> Maybe (Gen (input Symbolic))` | Generate an input, or `Nothing` if inapplicable |+| `lsCmdExec` | `input Concrete -> m output` | Execute against the real system |+| `lsCmdModel` | `forall v. Ord1 v => LockstepState model v -> input v -> (modelOutput, model)` | Pure model step |+| `lsCmdRequire` | `model -> input Symbolic -> Bool` | Additional preconditions |+| `lsCmdObserve` | `modelOutput -> output -> Test ()` | Compare model and real results |+| `lsCmdInvariants` | `model -> output -> Test ()` | System invariants beyond the lockstep check |+| `lsCmdTag` | `model -> model -> modelOutput -> [String]` | Per-step coverage tags (pre-state, post-state, model output) |++## Running tests++```haskell+-- Sequential (most common)+lockstepProperty     :: model -> Int -> [LockstepCmd (PropertyT IO) model] -> Property+lockstepPropertyWith :: model -> Int -> IO env -> (env -> IO ()) -> (env -> [LockstepCmd ...]) -> Property++-- Parallel (linearizability)+lockstepParallel     :: model -> Int -> Int -> [LockstepCmd (PropertyT IO) model] -> Property+lockstepParallelWith :: model -> Int -> Int -> IO env -> (env -> IO ()) -> (env -> [LockstepCmd ...]) -> Property++-- Manual (use Gen.sequential / executeSequential directly)+lockstepCommands :: [LockstepCmd m model] -> [Command Gen m (LockstepState model)]+```++Use the `*With` variants when commands need IO resources (e.g., `IORef`, database connections). The reset callback runs before each execution attempt, including during shrinking.++The bare `lockstepProperty` and `lockstepParallel` are for commands that don't need a resource. The commands still run in `PropertyT IO` (Hedgehog requires it), but `lsCmdExec` can simply lift a pure value with `pure`. See `test/Test/PureSort.hs` for a fully pure example.++Parallel operations must be thread-safe: use `atomicModifyIORef'`, `MVar`, or `TVar` rather than `modifyIORef'`.++### Running tests in your own monad++If your commands are written in a custom monad stack (e.g., `ReaderT Connection (PropertyT IO)`), use the `*M` variants to plug in a runner. They take a natural transformation that lowers your monad back to `PropertyT IO`:++```haskell+-- Sequential, in an arbitrary monad m+lockstepPropertyM+  :: (Show model, Monad m)+  => model -> Int+  -> (forall a. m a -> PropertyT IO a)  -- ^ how to run m+  -> [LockstepCmd m model]+  -> Property++-- With an IO resource: the runner receives the resource per test case+lockstepPropertyWithM+  :: (Show model, Monad m)+  => model -> Int+  -> IO env -> (env -> IO ())+  -> (forall a. env -> m a -> PropertyT IO a)+  -> (env -> [LockstepCmd m model])+  -> Property++-- Parallel variants: lockstepParallelM, lockstepParallelWithM+```++For a `ReaderT env (PropertyT IO)` stack the runner is just `flip runReaderT`:++```haskell+prop_kv :: Property+prop_kv =+  lockstepPropertyWithM+    Map.empty 50+    newStore resetStore+    (\store m -> runReaderT m store)+    (\_store -> [cmdPut, cmdGet])+```++Now the command bodies can `ask` the resource from the environment instead of closing over it. See `test/Test/ReaderKV.hs` for the full example.++## Coverage labels++There are two ways to get per-test coverage. Use whichever is more natural for the tag in question.++**`lsCmdTag`** is the dedicated per-step tagging hook (the analogue of `quickcheck-lockstep`'s `tagStep`). It receives the pre-step model, the post-step model, and the model's predicted output, and returns a list of string tags. Each tag is fed to `Hedgehog.label`. This is the right place for tags that depend on how the model state changed during the step.++```haskell+cmdPut store = LockstepCmd+  { ...+  , lsCmdTag = \pre post () ->+      ["Put", if Map.size post > Map.size pre then "Put new key" else "Put overwrite"]+  }+```++**`lsCmdObserve`** runs in `Test ()`, so Hedgehog's `label`, `classify`, and `cover` work directly inside it. Use this for tags that depend on the real output (which `lsCmdTag` doesn't see).++```haskell+cmdGet store = LockstepCmd+  { ...+  , lsCmdObserve = \expected actual -> do+      label "Get"+      classify "Get hit"  (isJust expected)+      classify "Get miss" (isNothing expected)+      expected === actual+  }+```++Hedgehog aggregates the labels across the run and prints a per-tag distribution table in the test summary. See `test/Test/KVStore.hs` for both styles.++### Labelled examples (model-only)++Hedgehog's distribution table tells you how often each tag fires across a real test run, but it doesn't show *what kind of trace* produced each tag. `lockstepLabelledExamples` does, by running the model side only (no IO) and printing one shortest sampled trace per tag:++```haskell+import Hedgehog.Lockstep++main :: IO ()+main = do+  _ <- lockstepLabelledExamples+         100         -- trials+         12          -- max actions per trial+         Map.empty   -- initial model+         [cmdPut, cmdDelete]+  pure ()+```++Sample output:++```+lockstepLabelledExamples: 4 tag(s) observed.+Tag "Put new key" (1 action(s)):+  PutInput "b" 18  [Put, Put new key]++Tag "Put overwrite" (2 action(s)):+  PutInput "a" 0   [Put, Put new key]+  PutInput "a" 12  [Put, Put overwrite]++...+```++This is the analogue of QuickCheck's `labelledExamples` and `quickcheck-lockstep`'s `tagActions`. Use it to confirm your generator and tagging actually exercise the cases you care about, before paying for a full property run. Because nothing real executes, `lsCmdExec` can be `error "unused"` if you want to write a coverage-only check.++## Failure diagnostics++When a test fails, `hedgehog-lockstep` automatically `footnote`s the post-step model state at every command. Hedgehog only displays footnotes on failure, so passing tests pay nothing, but a failing test now shows the model trail alongside the shrunken command sequence (the analogue of `quickcheck-lockstep`'s `monitoring` counterexample enrichment). This requires `Show model`, which is already needed by Hedgehog's `Gen.sequential`.++## System invariants++`lsCmdObserve` is for the lockstep equality check between the model output and the real output. For invariants on the post-state model itself (or on the real output independent of the model), use `lsCmdInvariants`. It receives the post-state model and the real output, runs in `Test ()`, and fires after every command.++```haskell+cmdSize store = LockstepCmd+  { ...+  , lsCmdObserve    = \expected actual -> expected === actual+  , lsCmdInvariants = \_ size -> assert (size >= 0)+  }+```++If you have nothing extra to check, write `lsCmdInvariants = \_ _ -> pure ()`.++## Building++Tested with GHC 9.6, 9.8, 9.10, and 9.12 (see `tested-with` in the cabal file for exact versions):++```+cabal build+cabal test+```++## Status++This is a v0.1 implementation.++### Known caveats++- **`Ord output` constraint**. `LockstepCmd` requires `Ord output` on command output types. This is needed for Var-identity-based model environment lookup. Most types satisfy this; truly opaque types (e.g., `IO.Handle`) would need a newtype wrapper that defines ordering (for example, by an allocation counter).++- **Depends on `Hedgehog.Internal.State`**. The library imports a handful of types and constructors (`Var`, `Symbolic`, `Concrete`, `Name`, `Command`, `Callback`) from Hedgehog's internal module because the public surface doesn't expose enough to drive the state machine framework directly. Hedgehog's PVP guarantees don't cover internal modules, so a Hedgehog minor release could in principle break the build. The cabal file pins `hedgehog >=1.4 && <1.6` to limit exposure; bump the upper bound only after rebuilding against the new version.++## License++BSD 3-Clause. See [LICENSE](LICENSE).
+ hedgehog-lockstep.cabal view
@@ -0,0 +1,109 @@+cabal-version:      3.0+name:               hedgehog-lockstep+version:            0.1.0.0+synopsis:           Lockstep-style stateful property testing for Hedgehog+description:+  Lockstep-style testing of stateful APIs built on Hedgehog's+  state machine framework. Ports the ideas of quickcheck-lockstep onto+  Hedgehog, giving integrated shrinking, parallel testing, and less+  boilerplate than the QuickCheck / quickcheck-dynamic / quickcheck-lockstep+  stack.++license:            BSD-3-Clause+license-file:       LICENSE+author:             Josh Burgess+maintainer:         joshualoganburgess@gmail.com+copyright:          (c) 2026 Josh Burgess+category:           Testing+homepage:           https://github.com/joshburgess/hedgehog-lockstep+bug-reports:        https://github.com/joshburgess/hedgehog-lockstep/issues+build-type:         Simple+extra-doc-files:+  CHANGELOG.md+  README.md++tested-with:+  GHC ==9.6.7+   || ==9.8.4+   || ==9.10.3+   || ==9.12.4++source-repository head+  type:     git+  location: https://github.com/joshburgess/hedgehog-lockstep.git++flag werror+  description: Turn warnings into errors (development only, not for releases).+  default:     False+  manual:      True++common warnings+  ghc-options:+    -Wall -Wcompat -Wno-unticked-promoted-constructors+    -funbox-strict-fields++  if flag(werror)+    ghc-options: -Werror++library+  import:           warnings+  hs-source-dirs:   src+  default-language: GHC2021+  default-extensions:+    DerivingStrategies+    GADTs+    LambdaCase+    OverloadedStrings+    RecordWildCards+    StrictData++  exposed-modules:+    Hedgehog.Lockstep+    Hedgehog.Lockstep.Command+    Hedgehog.Lockstep.Examples+    Hedgehog.Lockstep.GVar+    Hedgehog.Lockstep.Observe+    Hedgehog.Lockstep.Op+    Hedgehog.Lockstep.Property+    Hedgehog.Lockstep.State++  build-depends:+    , barbies    >=2.0     && <2.2+    , base       >=4.18    && <4.22+    , containers >=0.6     && <0.9+    , hedgehog   >=1.4     && <1.6++test-suite hedgehog-lockstep-test+  import:           warnings+  type:             exitcode-stdio-1.0+  hs-source-dirs:   test+  main-is:          Main.hs+  default-language: GHC2021+  default-extensions:+    DerivingStrategies+    GADTs+    LambdaCase+    OverloadedStrings+    RecordWildCards+    StrictData++  other-modules:+    Test.BuggyCounter+    Test.CustomOp+    Test.HandleStore+    Test.KVStore+    Test.LabelledExamples+    Test.Observation+    Test.OpProjections+    Test.ParallelKV+    Test.PureSort+    Test.ReaderKV+    Test.UnitCoverage++  build-depends:+    , base              >=4.18 && <4.22+    , barbies           >=2.0  && <2.2+    , containers        >=0.6  && <0.9+    , hedgehog          >=1.4  && <1.6+    , hedgehog-lockstep+    , mtl               >=2.2  && <2.4
+ src/Hedgehog/Lockstep.hs view
@@ -0,0 +1,95 @@+-- | Lockstep-style stateful property testing for Hedgehog.+--+-- This is the top-level facade. Most users will only need to import this+-- module. It re-exports the public API of 'Hedgehog.Lockstep.Command',+-- 'Hedgehog.Lockstep.Property', 'Hedgehog.Lockstep.State',+-- 'Hedgehog.Lockstep.GVar', and 'Hedgehog.Lockstep.Op', plus the small+-- set of Hedgehog and barbies identifiers needed to write commands.+--+-- A short tour:+--+-- * t'LockstepCmd' is the unit of testing: an API operation with its+--   model interpretation, observation, and invariants.+-- * 'lockstepProperty' / 'lockstepPropertyWith' run sequential tests.+-- * 'lockstepParallel' / 'lockstepParallelWith' run linearizability tests.+-- * t'GVar' with t'Op' projects values out of compound action outputs so+--   later commands can refer to them.+--+-- See the README and "Hedgehog.Lockstep.Command" for fuller explanations.+module Hedgehog.Lockstep+  ( -- * Commands+    LockstepCmd (..)+  , toLockstepCommand+  , hoistLockstepCmd+  , lockstepCommands++    -- * State+  , LockstepState+  , ModelEnv+  , initialLockstepState+  , getModel+  , getEntries+  , varsOfType++    -- * Generalized variables+  , GVar (..)+  , mkGVar+  , mkGVarId+  , mapGVar+  , resolveGVar+  , concreteGVar+  , gvarLabel++    -- * Structural projections+  , Op (..)+  , InterpretOp (..)+  , applyOp+  , (>>>)++    -- * Structured observations+  , Observation (..)+  , runObservation++    -- * Running tests+  , lockstepProperty+  , lockstepPropertyWith+  , lockstepParallel+  , lockstepParallelWith++    -- * Running tests in arbitrary monads+  , lockstepPropertyM+  , lockstepPropertyWithM+  , lockstepParallelM+  , lockstepParallelWithM++    -- * Coverage exploration+  , lockstepLabelledExamples+  , LabelledExamples+  , ModelStep (..)++    -- * Re-exports from Hedgehog+  , Var (..)+  , Symbolic+  , Concrete+  , Gen+  , Test+  , Property+  , PropertyT+  , (===)++    -- * Re-exports from barbies+  , FunctorB (..)+  , TraversableB (..)+  ) where++import Data.Functor.Barbie (FunctorB (..), TraversableB (..))+import Hedgehog (Gen, Test, Property, PropertyT, (===))+import Hedgehog.Internal.State (Var (..), Symbolic, Concrete)++import Hedgehog.Lockstep.Op+import Hedgehog.Lockstep.GVar+import Hedgehog.Lockstep.Observe+import Hedgehog.Lockstep.State+import Hedgehog.Lockstep.Command+import Hedgehog.Lockstep.Examples+import Hedgehog.Lockstep.Property
+ src/Hedgehog/Lockstep/Command.hs view
@@ -0,0 +1,224 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | The t'LockstepCmd' record bundling a single API operation with its+-- model interpretation, observation, and post-state invariants.+--+-- Construct one t'LockstepCmd' per operation in your API. Convert the+-- list to Hedgehog t'Hedgehog.Internal.State.Command's via+-- 'toLockstepCommand' (or use+-- 'Hedgehog.Lockstep.Property.lockstepCommands' to do it in bulk).+module Hedgehog.Lockstep.Command+  ( LockstepCmd (..)+  , toLockstepCommand+  , hoistLockstepCmd+  ) where++import Data.Dynamic (dynTypeRep, fromDynamic)+import Data.Proxy (Proxy (..))+import Data.String (fromString)+import Data.Typeable (TypeRep, Typeable, typeRep)+import Data.Functor.Barbie (TraversableB)+import Data.Functor.Classes (Ord1)+import Hedgehog (Gen, Test, footnote, failure, label)+import Hedgehog.Internal.State+  ( Command (..)+  , Callback (..)+  , Symbolic+  , Concrete+  )++import Hedgehog.Lockstep.State++-- | A lockstep command packages a single API operation with its model+-- interpretation and observation function.+--+-- The key idea: in the 'Update' callback, the library runs 'lsCmdModel' to+-- advance the model state and stores the model result. In 'Ensure', it+-- retrieves the stored model result and compares it with the real output+-- via 'lsCmdObserve'.+--+-- == Type constraints+--+-- The existential constraints on @output@ and @modelOutput@ are:+--+-- * @'Typeable' output@, @'Ord' output@: required by the model environment,+--   which keys entries by 'Hedgehog.Internal.State.Var' identity. The 'Ord'+--   instance is used by 'Data.Functor.Classes.Ord1' for phase-polymorphic+--   'Hedgehog.Internal.State.Var' comparison.+--+-- * @'Typeable' modelOutput@, @'Eq' modelOutput@, @'Show' modelOutput@: the+--   model-side result is stored as 'Data.Dynamic.Dynamic' and may be compared+--   or displayed in error reports.+--+-- The @'Ord' output@ constraint is a real limitation: truly opaque types like+-- @'System.IO.Handle'@ that lack an 'Ord' instance need a newtype wrapper that+-- defines ordering (for example, by an allocation counter).+data LockstepCmd m model = forall input output modelOutput.+  ( TraversableB input+  , Show (input Symbolic)+  , Show output+  , Typeable output+  , Ord output+  , Typeable modelOutput+  , Eq modelOutput+  , Show modelOutput+  ) => LockstepCmd+  { -- | Generate an input given the current lockstep state.+    -- Return 'Nothing' if this command is not applicable in the current state.+    lsCmdGen :: LockstepState model Symbolic -> Maybe (Gen (input Symbolic))++    -- | Execute the command against the real system.+  , lsCmdExec :: input Concrete -> m output++    -- | Run the model step. Given the current lockstep state and input,+    -- return the model's predicted output and the updated model.+    --+    -- This runs in @forall v. Ord1 v@ context. Use+    -- 'Hedgehog.Lockstep.GVar.resolveGVar' with+    -- 'Hedgehog.Lockstep.State.getEntries' to resolve+    -- t'Hedgehog.Lockstep.GVar.GVar's in the input to their model values.+  , lsCmdModel :: forall v. Ord1 v => LockstepState model v -> input v -> (modelOutput, model)++    -- | Additional preconditions beyond variable-definedness.+  , lsCmdRequire :: model -> input Symbolic -> Bool++    -- | Compare model output with real output.+    -- Use Hedgehog assertions ('Hedgehog.===' etc.) to report mismatches.+    --+    -- For structured comparison patterns (equality, projection,+    -- pairwise), 'Hedgehog.Lockstep.Observe.runObservation' produces+    -- a function of exactly this type from a typed+    -- 'Hedgehog.Lockstep.Observe.Observation' value, so you can write+    --+    -- > lsCmdObserve = runObservation ObserveEq+    --+    -- or+    --+    -- > lsCmdObserve = runObservation (ObserveProject normModel normReal)+    --+    -- instead of writing the assertion by hand.+  , lsCmdObserve :: modelOutput -> output -> Test ()++    -- | Additional invariants to check after each command, separate from+    -- the lockstep model-vs-real equality check in 'lsCmdObserve'.+    --+    -- Receives the post-state model and the real output. Use this for+    -- system invariants that hold regardless of the lockstep comparison+    -- (for example, "size never goes negative" or "no orphan handles").+    --+    -- Use @\\_ _ -> 'pure' ()@ if you have nothing extra to check.+  , lsCmdInvariants :: model -> output -> Test ()++    -- | Optional per-step coverage tags. Receives the pre-step model state,+    -- the post-step model state, and the model's predicted output. Returns+    -- a list of string tags; each tag becomes a 'Hedgehog.label' call so the+    -- test summary reports per-tag distribution.+    --+    -- This is the 'hedgehog-lockstep' analogue of @quickcheck-lockstep@'s+    -- @tagStep@. Calling 'Hedgehog.label' or 'Hedgehog.classify' inside+    -- 'lsCmdObserve' also works for ad-hoc coverage, but 'lsCmdTag' is the+    -- natural place for tags whose value depends on how the model state+    -- changed during this step (e.g., \"insert into empty\",+    -- \"delete present key\", \"size grew past threshold\").+    --+    -- Use @\\_ _ _ -> []@ if you don't need coverage tagging.+  , lsCmdTag :: model -> model -> modelOutput -> [String]+  }++-- | Convert a t'LockstepCmd' into a Hedgehog+-- t'Hedgehog.Internal.State.Command'.+--+-- The resulting command's @Ensure@ callback always 'Hedgehog.footnote's+-- the post-step model. Hedgehog only displays footnotes when a test+-- fails, so this gives a free post-mortem trace of the model state+-- evolution while costing nothing for passing tests. This is the+-- analogue of @quickcheck-lockstep@'s @monitoring@ counterexample+-- enrichment.+toLockstepCommand+  :: (Show model, Monad m)+  => LockstepCmd m model -> Command Gen m (LockstepState model)+{-# INLINABLE toLockstepCommand #-}+toLockstepCommand (LockstepCmd{..}) = Command gen exec callbacks+  where+    gen st = lsCmdGen st++    exec = lsCmdExec++    callbacks =+      [ Require $ \st input ->+          lsCmdRequire (lsModel st) input++      , Update $ \st input var ->+          let (modelOut, model') = lsCmdModel st input+          in insertModelResult var modelOut (st { lsModel = model' })++      , Ensure $ \oldSt newSt _input output -> do+          -- Model-state footnote: only displayed on failure, so this is+          -- effectively free for passing tests but gives a state trace+          -- when something goes wrong.+          footnote $ "model post-step: " <> show (lsModel newSt)+          -- The most recently inserted model result corresponds to+          -- this action. 'lsLastEntry' is set by 'insertModelResult'+          -- in the matching 'Update' callback above.+          case lsLastEntry newSt of+            Just dyn ->+              case fromDynamic dyn of+                Just modelOut -> do+                  -- Coverage tagging fires before observation so that+                  -- the test report records the tag even on the test+                  -- run that shrinks down to the failing example.+                  mapM_ (label . fromString) $+                    lsCmdTag (lsModel oldSt) (lsModel newSt) modelOut+                  lsCmdObserve modelOut output+                  lsCmdInvariants (lsModel newSt) output+                Nothing -> do+                  footnote $ unlines+                    [ "hedgehog-lockstep internal error: model result type mismatch."+                    , "  stored Dynamic type: " <> show (dynTypeRep dyn)+                    , "  expected:            " <> show (expectedModelType lsCmdObserve)+                    , "This indicates the Update and Ensure callbacks for one"+                    , "command saw inconsistent types, which should be impossible."+                    ]+                  failure+            Nothing -> do+              -- Unreachable: Hedgehog runs Update before Ensure for the+              -- same command, and Update always sets 'lsLastEntry' via+              -- 'insertModelResult'.+              footnote "hedgehog-lockstep internal error: Ensure ran without a preceding Update"+              failure+      ]++-- | Recover the model-output 'TypeRep' from a 'lsCmdObserve' function,+-- so that internal-error messages can name the type the 'Ensure' callback+-- expected to find in the stored 'Data.Dynamic.Dynamic'.+expectedModelType+  :: forall modelOutput output. Typeable modelOutput+  => (modelOutput -> output -> Test ()) -> TypeRep+expectedModelType _ = typeRep (Proxy @modelOutput)++-- | Transform the monad of a t'LockstepCmd' by lifting the exec function+-- through a natural transformation @m -> n@.+--+-- This is the hook that lets users write commands in a monad of their+-- choice (e.g., @'Control.Monad.Reader.ReaderT' Connection ('Hedgehog.PropertyT' 'IO')@)+-- while still running them with hedgehog's runner, which expects+-- @'Hedgehog.PropertyT' 'IO'@. The monad-parameterized runners+-- ('Hedgehog.Lockstep.Property.lockstepPropertyM' and friends) use+-- 'hoistLockstepCmd' under the hood.+--+-- All other fields are preserved unchanged.+hoistLockstepCmd+  :: (forall a. m a -> n a)+  -> LockstepCmd m model+  -> LockstepCmd n model+hoistLockstepCmd nat LockstepCmd{..} = LockstepCmd+  { lsCmdGen        = lsCmdGen+  , lsCmdExec       = nat . lsCmdExec+  , lsCmdModel      = lsCmdModel+  , lsCmdRequire    = lsCmdRequire+  , lsCmdObserve    = lsCmdObserve+  , lsCmdInvariants = lsCmdInvariants+  , lsCmdTag        = lsCmdTag+  }+{-# INLINABLE hoistLockstepCmd #-}
+ src/Hedgehog/Lockstep/Examples.hs view
@@ -0,0 +1,192 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Model-only driver for collecting one shortest example per tag.+--+-- 'lockstepLabelledExamples' generates random command sequences,+-- /runs only the model side/, accumulates the tags emitted by+-- 'Hedgehog.Lockstep.Command.lsCmdTag', and prints one shortest+-- trace per tag observed. This is the analogue of+-- @QuickCheck@'s @labelledExamples@ and+-- @quickcheck-lockstep@'s @tagActions@: it answers \"is the test+-- generator actually exercising the labelled cases I care about?\"+-- without paying the cost of executing the real system.+--+-- The function never fails. It always prints something. It returns+-- the collected examples as a 'Data.Map.Strict.Map' so callers can+-- post-process them programmatically as well.+module Hedgehog.Lockstep.Examples+  ( lockstepLabelledExamples+  , LabelledExamples+  , ModelStep (..)+  ) where++import Control.Monad (forM_)+import Data.Foldable (for_)+import Data.IORef (IORef, modifyIORef', newIORef, readIORef)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (mapMaybe)+import Hedgehog (Gen)+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range+import Hedgehog.Internal.State (Name (..), Symbolic (..), Var (..))+import Hedgehog.Internal.State qualified++import Hedgehog.Lockstep.Command (LockstepCmd (..))+import Hedgehog.Lockstep.State+  ( LockstepState (..)+  , initialLockstepState+  , insertModelResult+  )++-- | One step in a sampled trace: the rendered (symbolic) input and the+-- list of tags it produced via 'Hedgehog.Lockstep.Command.lsCmdTag'.+data ModelStep = ModelStep+  { stepRendered :: !String+    -- ^ The input rendered via @show@ (the @Show (input Symbolic)@+    -- instance required by 'Hedgehog.Lockstep.Command.LockstepCmd').+  , stepTags     :: ![String]+    -- ^ Tags emitted by 'Hedgehog.Lockstep.Command.lsCmdTag' for this step.+  }+  deriving stock (Show)++-- | A map from tag to the shortest sampled trace that produced it.+--+-- The key is the tag string. The value is the trace, ordered earliest+-- step first, and \"shortest\" is measured by total step count: ties+-- are broken by first-seen.+type LabelledExamples = Map String [ModelStep]++-- | Sample @nTrials@ random command sequences (model-only) of up to+-- @maxActions@ steps each. Collect every tag emitted by+-- 'Hedgehog.Lockstep.Command.lsCmdTag' along the way, keeping the+-- shortest trace seen for each tag. Print the collected examples and+-- return them.+--+-- This runs entirely in the model: 'Hedgehog.Lockstep.Command.lsCmdExec'+-- is /not/ called, so no IO resources or real systems are involved.+-- Use it as a sanity check that your generator and tagging cover the+-- cases you expect, before spending CPU on a real test run.+--+-- The output format is one block per tag:+--+-- @+-- Tag \"Put new key\" (3 actions):+--   PutInput \"a\" 5      [Put, Put new key]+--   GetInput \"b\"        [Get]+--   DeleteInput \"a\"     [Delete]+-- @+--+-- Tags listed on a step are exactly those returned by+-- 'Hedgehog.Lockstep.Command.lsCmdTag' for that step.+lockstepLabelledExamples+  :: forall m model.+     Int+     -- ^ Number of random trials (e.g., @1000@)+  -> Int+     -- ^ Max actions per trial (e.g., @20@)+  -> model+     -- ^ Initial model+  -> [LockstepCmd m model]+     -- ^ Commands (the @m@ parameter is ignored: model-only run)+  -> IO LabelledExamples+lockstepLabelledExamples nTrials maxActions model0 cmds = do+  ref <- newIORef Map.empty+  let trial = do+        steps <- Gen.sample (sampleTrace maxActions model0 cmds)+        recordTrace ref steps+  -- replicateM_ would suffice, but keep it explicit for readability:+  forM_ [1 .. nTrials] $ \_ -> trial+  examples <- readIORef ref+  printExamples examples+  pure examples++-- | Record one trace into the running collection: for every tag the+-- trace produced, keep this trace if it's the first or strictly+-- shorter than the previously stored one.+recordTrace :: IORef LabelledExamples -> [ModelStep] -> IO ()+recordTrace ref steps =+  let tagsHere = concatMap stepTags steps+      len      = length steps+      improve mb = case mb of+        Nothing                         -> Just steps+        Just prev | length prev > len   -> Just steps+                  | otherwise           -> mb+  in for_ tagsHere $ \tag ->+       modifyIORef' ref (Map.alter improve tag)++printExamples :: LabelledExamples -> IO ()+printExamples examples+  | Map.null examples =+      putStrLn "lockstepLabelledExamples: no tags emitted by lsCmdTag."+  | otherwise = do+      putStrLn $ "lockstepLabelledExamples: "+              <> show (Map.size examples)+              <> " tag(s) observed."+      forM_ (Map.toList examples) $ \(tag, steps) -> do+        putStrLn $ "Tag \"" <> tag <> "\" (" <> show (length steps) <> " action(s)):"+        forM_ steps $ \step -> do+          let tagSuffix = case stepTags step of+                [] -> ""+                ts -> "  [" <> commaJoin ts <> "]"+          putStrLn $ "  " <> stepRendered step <> tagSuffix+        putStrLn ""++commaJoin :: [String] -> String+commaJoin []       = ""+commaJoin [x]      = x+commaJoin (x : xs) = x <> ", " <> commaJoin xs++-- ---------------------------------------------------------------------------+-- Sampler: walks one model-only trace.+-- ---------------------------------------------------------------------------++-- | Generate one trace of up to @maxActions@ steps by walking the model.+sampleTrace+  :: forall m model.+     Int+  -> model+  -> [LockstepCmd m model]+  -> Gen [ModelStep]+sampleTrace maxActions model0 cmds = do+  n <- Gen.int (Range.linear 1 maxActions)+  go n (initialLockstepState model0)+  where+    go :: Int -> LockstepState model Symbolic -> Gen [ModelStep]+    go 0 _ = pure []+    go k st =+      case mapMaybe (`stepFor` st) cmds of+        []      -> pure []+        choices -> do+          stepGen <- Gen.element choices+          mResult <- stepGen+          case mResult of+            Nothing            -> pure []+            Just (st', step)   -> (step :) <$> go (k - 1) st'++-- | If @cmd@ is applicable in @st@, return a generator that produces+-- the post-step state and the rendered step (or 'Nothing' if the+-- precondition rejects the input post-generation).+stepFor+  :: forall m model.+     LockstepCmd m model+  -> LockstepState model Symbolic+  -> Maybe (Gen (Maybe (LockstepState model Symbolic, ModelStep)))+stepFor cmd st =+  case cmd of+    LockstepCmd lsCmdGen (_ :: input Hedgehog.Internal.State.Concrete -> m output)+                lsCmdModel lsCmdRequire _ _ lsCmdTag -> do+      inputGen <- lsCmdGen st+      Just $ do+        input <- inputGen+        if not (lsCmdRequire (lsModel st) input)+          then pure Nothing+          else do+            let varId           = lsNextVarId st+                var :: Var output Symbolic+                var             = Var (Symbolic (Name varId))+                (modelOut, m')  = lsCmdModel st input+                st'             = insertModelResult var modelOut (st { lsModel = m' })+                tags            = lsCmdTag (lsModel st) m' modelOut+                rendered        = show input+            pure (Just (st', ModelStep rendered tags))
+ src/Hedgehog/Lockstep/GVar.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE RankNTypes #-}+-- | Generalized variables: typed projections from prior action outputs.+--+-- A t'GVar' wraps a Hedgehog t'Hedgehog.Internal.State.Var' together with+-- an 'Hedgehog.Lockstep.Op.Op' that projects a component out of the+-- action's result. Later commands use t'GVar's to refer to those+-- components in both the model and the real system.+module Hedgehog.Lockstep.GVar+  ( GVar (..)+  , mkGVar+  , mkGVarId+  , mapGVar+  , resolveGVar+  , concreteGVar+  , gvarLabel+  ) where++import Data.Dynamic (Dynamic, fromDynamic, toDyn)+import Data.Typeable (Typeable)+import Data.Functor.Classes (Ord1)+import Hedgehog.Internal.State (Var (..), Concrete (..))+import Data.Functor.Barbie (FunctorB (..), TraversableB (..))++import Hedgehog.Lockstep.Op (InterpretOp, interpretOp)+import Hedgehog.Lockstep.State (ModelEnv, lookupModelEntry)++-- | A generalized variable that projects a value of type @a@ from a+-- previous action's output via the model environment.+--+-- During generation (t'Hedgehog.Internal.State.Symbolic' phase), the+-- t'GVar' tracks which variable it references. During execution+-- (t'Hedgehog.Internal.State.Concrete' phase), the underlying t'Hedgehog.Internal.State.Var'+-- resolves to the real value, but model-side resolution always goes+-- through the model environment via t'Hedgehog.Internal.State.Var'+-- identity matching.+data GVar a v where+  GVar+    :: (Typeable x, Ord x)+    => !(Var x v)                  -- ^ Underlying Hedgehog variable+    -> !String                     -- ^ Human-readable projection label+    -> !(Dynamic -> Maybe a)       -- ^ Resolution function from model env entry+    -> GVar a v++instance FunctorB (GVar a) where+  bmap f (GVar (Var v) label res) = GVar (Var (f v)) label res++instance TraversableB (GVar a) where+  btraverse f (GVar (Var v) label res) =+    (\v' -> GVar (Var v') label res) <$> f v++instance Show (GVar a v) where+  show (GVar _ label _) = "GVar." <> label++-- | Construct a t'GVar' using a typed structural projection.+--+-- @modelX@ is the model-side output type stored in the environment.+-- The op projects from @modelX@ to the desired type @a@. Any op type with+-- an 'InterpretOp' instance and a 'Show' instance works here. The library+-- ships 'Hedgehog.Lockstep.Op.Op' as the default; users can extend the+-- projection vocabulary by defining their own GADT.+mkGVar+  :: (Typeable modelX, Typeable realX, Ord realX, InterpretOp op, Show (op modelX a))+  => Var realX v -> op modelX a -> GVar a v+mkGVar var op =+  GVar var (show op) $ \dyn ->+    fromDynamic dyn >>= interpretOp op+{-# INLINABLE mkGVar #-}++-- | Construct a t'GVar' with an identity projection. Use when the+-- entire model output is the desired value.+mkGVarId+  :: (Typeable a, Typeable realX, Ord realX)+  => Var realX v -> GVar a v+mkGVarId var =+  GVar var "id" fromDynamic+{-# INLINABLE mkGVarId #-}++-- | Compose an additional projection onto an existing t'GVar'.+--+-- Useful when you already hold a t'GVar' to a structured value and want+-- to project further. For example, given a @t'GVar' ('Either' err (h, name)) v@,+-- @'mapGVar' ('Hedgehog.Lockstep.Op.OpRight' 'Hedgehog.Lockstep.Op.>>>' 'Hedgehog.Lockstep.Op.OpFst')@+-- produces a @t'GVar' h v@.+--+-- The new t'GVar' shares the underlying Hedgehog t'Hedgehog.Internal.State.Var'+-- and the existing resolution chain; only the final projection step+-- changes. The human-readable label is extended with the new op.+--+-- This is the 'hedgehog-lockstep' analogue of @quickcheck-lockstep@'s+-- @mapGVar@.+mapGVar+  :: forall op a b v. (InterpretOp op, Show (op a b))+  => op a b -> GVar a v -> GVar b v+mapGVar op (GVar var label resolve) =+  GVar var (label <> "." <> show op) (\dyn -> resolve dyn >>= interpretOp op)+{-# INLINABLE mapGVar #-}++-- | Resolve a t'GVar' against a model environment.+-- Uses 'Ord1' for phase-polymorphic t'Hedgehog.Internal.State.Var'+-- comparison.+resolveGVar :: Ord1 v => GVar a v -> ModelEnv v -> Maybe a+resolveGVar (GVar var _ resolve) entries =+  lookupModelEntry var entries >>= resolve+{-# INLINABLE resolveGVar #-}++-- | Extract the projected value from a t'GVar' in the t'Hedgehog.Internal.State.Concrete' phase.+--+-- This applies the resolution function to the real output value. Works when+-- the real and model types share the same structure at the projected position+-- (e.g., both are @Either String (Int, String)@).+concreteGVar :: GVar a Concrete -> Maybe a+concreteGVar (GVar (Var (Concrete x)) _ resolve) = resolve (toDyn x)+{-# INLINABLE concreteGVar #-}++-- | Get the human-readable label of a t'GVar'.+gvarLabel :: GVar a v -> String+gvarLabel (GVar _ label _) = label
+ src/Hedgehog/Lockstep/Observe.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE GADTs #-}+-- | Structured comparison of model output and real output.+--+-- A t'Observation' value describes /how/ to compare a model-side output+-- (of type @modelOutput@) against the real system's output (of type+-- @output@), without committing to a specific assertion at the call+-- site. The 'runObservation' function turns an t'Observation' into a+-- function suitable for the+-- 'Hedgehog.Lockstep.Command.lsCmdObserve' field of+-- 'Hedgehog.Lockstep.Command.LockstepCmd'.+--+-- This is the 'hedgehog-lockstep' analogue of+-- @quickcheck-lockstep@'s @Observable@\/@ModelValue@ GADT split:+-- t'Observation' factors out the "what does it mean for these two values+-- to agree?" question into a small typed DSL with three primitives+-- ('ObserveEq', 'ObserveProject', 'ObserveCustom') and one combinator+-- ('ObservePair'), all driven by hedgehog's diffable equality+-- ('Hedgehog.===').+--+-- == Why bother+--+-- Plain @lsCmdObserve = (===)@ requires the model and real outputs to+-- have the same type. Real APIs frequently violate that:+--+-- * The real side returns an opaque handle while the model returns an+--   index.+-- * The real side returns a concrete error message while the model+--   returns an abstract error tag.+-- * Both sides return rich records but only a few fields should be+--   compared.+--+-- 'ObserveProject' addresses these by pushing both sides through+-- normalising functions before comparing. 'ObservePair' composes two+-- observations on a tuple. 'ObserveCustom' is the escape hatch when+-- nothing else fits.+module Hedgehog.Lockstep.Observe+  ( Observation (..)+  , runObservation+  ) where++import Hedgehog (Test, (===))++-- | A typed description of how to compare a model output of type+-- @modelOutput@ against a real output of type @output@.+--+-- All constructors carry the 'Eq' and 'Show' instances needed to+-- produce hedgehog's standard diff on mismatch.+data Observation modelOutput output where+  -- | The model and real outputs have the same type and should be+  -- compared by equality. This is the common case for pure model+  -- predictions.+  ObserveEq+    :: (Eq output, Show output)+    => Observation output output++  -- | Project each side through a normalising function and compare the+  -- projections by equality. Use this when the two sides have different+  -- types but a meaningful common observation: comparing only the+  -- relevant fields, normalising error formats, etc.+  --+  -- The two projections @modelOutput -> obs@ and @output -> obs@ must+  -- agree on what counts as "the same" result.+  ObserveProject+    :: (Eq obs, Show obs)+    => (modelOutput -> obs)+    -> (output -> obs)+    -> Observation modelOutput output++  -- | Apply two observations componentwise to a pair. Useful when an+  -- action returns a tuple where each side wants its own normalisation.+  ObservePair+    :: Observation m1 o1+    -> Observation m2 o2+    -> Observation (m1, m2) (o1, o2)++  -- | Drop down to an arbitrary 'Test' action for cases that none of+  -- the structured constructors capture (custom diff messages,+  -- multi-step assertions, classification side-effects, etc.).+  ObserveCustom+    :: (modelOutput -> output -> Test ())+    -> Observation modelOutput output++-- | Interpret an t'Observation' as a check that the model and real+-- outputs agree.+--+-- The result is intentionally shaped to match+-- 'Hedgehog.Lockstep.Command.lsCmdObserve' so users can write+--+-- > lsCmdObserve = runObservation (ObserveProject normaliseModel normaliseReal)+--+-- and skip writing the @===@ call by hand.+runObservation :: Observation modelOutput output -> modelOutput -> output -> Test ()+runObservation obs0 = go obs0+  where+    go :: Observation m o -> m -> o -> Test ()+    go ObserveEq                   m o            = m === o+    go (ObserveProject pm po)      m o            = pm m === po o+    go (ObservePair obsA obsB)     (m1, m2) (o1, o2) = do+      go obsA m1 o1+      go obsB m2 o2+    go (ObserveCustom k)           m o            = k m o+{-# INLINABLE runObservation #-}
+ src/Hedgehog/Lockstep/Op.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE PolyKinds #-}+-- | Structural projections used with 'Hedgehog.Lockstep.GVar.GVar' to+-- extract components from compound action outputs.+--+-- The library ships a default 'Op' GADT covering pair, sum, identity, and+-- composition. Users who need additional projections (list head, record+-- field, etc.) can define their own GADT and provide an 'InterpretOp'+-- instance. 'Hedgehog.Lockstep.GVar.mkGVar' and+-- 'Hedgehog.Lockstep.GVar.mapGVar' accept any op with an 'InterpretOp' and+-- 'Show' instance.+--+-- For example, if an action returns @'Either' err ('Hedgehog.Internal.State.Var' h, name)@,+-- the projection @'OpRight' '>>>' 'OpFst'@ extracts the @h@.+module Hedgehog.Lockstep.Op+  ( -- * The default 'Op' GADT+    Op (..)+  , (>>>)++    -- * Extensibility+  , InterpretOp (..)+  , applyOp+  , showOp+  ) where++-- | Interpret a structural projection as a partial function on values.+--+-- Implementations return 'Nothing' for projections that don't apply to the+-- input value (e.g., 'OpLeft' applied to a 'Right'). Compose your own op+-- GADT and provide an instance to extend the projection vocabulary beyond+-- 'Op'. The library imposes no restriction on the kind or shape of @op@:+-- typical instances are GADTs of kind @'Data.Kind.Type' -> 'Data.Kind.Type' -> 'Data.Kind.Type'@.+class InterpretOp op where+  interpretOp :: op a b -> a -> Maybe b++-- | The default structural projections: identity, pair, sum, composition.+--+-- This covers the common cases of projecting from a tuple or @'Either'@.+-- For richer projections (list head, record field, custom decoders, etc.)+-- define your own op GADT and provide an 'InterpretOp' instance, then pass+-- it to 'Hedgehog.Lockstep.GVar.mkGVar' or+-- 'Hedgehog.Lockstep.GVar.mapGVar' just like 'Op'.+--+-- 'OpLeft' and 'OpRight' are partial: 'interpretOp' returns 'Nothing' if+-- the 'Either' doesn't match.+data Op a b where+  OpId    :: Op a a+  OpFst   :: Op (a, b) a+  OpSnd   :: Op (a, b) b+  OpLeft  :: Op (Either a b) a+  OpRight :: Op (Either a b) b+  OpComp  :: !(Op b c) -> !(Op a b) -> Op a c++instance InterpretOp Op where+  interpretOp OpId x = Just x+  interpretOp OpFst (a, _) = Just a+  interpretOp OpSnd (_, b) = Just b+  interpretOp OpLeft (Left a) = Just a+  interpretOp OpLeft (Right _) = Nothing+  interpretOp OpRight (Left _) = Nothing+  interpretOp OpRight (Right b) = Just b+  interpretOp (OpComp f g) x = interpretOp g x >>= interpretOp f+  {-# INLINABLE interpretOp #-}++instance Show (Op a b) where+  show OpId         = "id"+  show OpFst        = "fst"+  show OpSnd        = "snd"+  show OpLeft       = "left"+  show OpRight      = "right"+  show (OpComp f g) = show g <> "." <> show f++-- | Left-to-right composition of 'Op's.+(>>>) :: Op a b -> Op b c -> Op a c+f >>> g = OpComp g f+infixr 1 >>>++-- | Apply a structural projection. Synonym for 'interpretOp' kept for the+-- pre-0.2 name.+applyOp :: InterpretOp op => op a b -> a -> Maybe b+applyOp = interpretOp+{-# INLINE applyOp #-}++-- | Render an op as a string. Synonym for 'show' kept for the pre-0.2 name.+showOp :: Show (op a b) => op a b -> String+showOp = show+{-# INLINE showOp #-}
+ src/Hedgehog/Lockstep/Property.hs view
@@ -0,0 +1,254 @@+{-# LANGUAGE RankNTypes #-}+-- | Property runners that turn a list of 'Hedgehog.Lockstep.Command.LockstepCmd'+-- values into a Hedgehog 'Hedgehog.Property'.+--+-- The @With@ variants set up an IO resource (an 'Data.IORef.IORef', a+-- database handle, etc.) that the commands use; the bare variants are for+-- commands that don't need one. The parallel variants generate concurrent+-- suffixes and check linearizability via Hedgehog's @executeParallel@.+module Hedgehog.Lockstep.Property+  ( lockstepProperty+  , lockstepPropertyWith+  , lockstepParallel+  , lockstepParallelWith+  , lockstepPropertyM+  , lockstepPropertyWithM+  , lockstepParallelM+  , lockstepParallelWithM+  , lockstepCommands+  ) where++import Hedgehog+  ( Gen+  , Property+  , PropertyT+  , property+  , forAll+  , evalIO+  , executeSequential+  , executeParallel+  )+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range+import Hedgehog.Internal.State (Command)++import Hedgehog.Lockstep.State (LockstepState, initialLockstepState)+import Hedgehog.Lockstep.Command (LockstepCmd, hoistLockstepCmd, toLockstepCommand)++-- | Convert a list of 'LockstepCmd's into Hedgehog+-- 'Hedgehog.Internal.State.Command's.+lockstepCommands+  :: (Show model, Monad m)+  => [LockstepCmd m model] -> [Command Gen m (LockstepState model)]+lockstepCommands = map toLockstepCommand+{-# INLINABLE lockstepCommands #-}++-- | Run a sequential lockstep property test (pure commands).+--+-- For commands that need IO resources (e.g., @IORef@), use+-- 'lockstepPropertyWith' instead.+lockstepProperty+  :: Show model+  => model+  -> Int+  -> [LockstepCmd (PropertyT IO) model]+  -> Property+lockstepProperty model0 maxActions cmds = property $ do+  let commands = lockstepCommands cmds+  actions <- forAll $+    Gen.sequential (Range.linear 1 maxActions) (initialLockstepState model0) commands+  executeSequential (initialLockstepState model0) actions+{-# INLINABLE lockstepProperty #-}++-- | Run a sequential lockstep property test with IO-based resource setup.+--+-- The @IO env@ action creates a fresh resource before generation.+-- The @env -> IO ()@ action resets the resource before execution+-- (needed because hedgehog reuses IO effects across shrink attempts).+-- The @env -> [LockstepCmd ...]@ function creates commands using the resource.+lockstepPropertyWith+  :: Show model+  => model+  -> Int+  -> IO env+  -- ^ Create resource (runs once per test case)+  -> (env -> IO ())+  -- ^ Reset resource (runs before each execution, including shrink attempts)+  -> (env -> [LockstepCmd (PropertyT IO) model])+  -- ^ Commands using the resource+  -> Property+lockstepPropertyWith model0 maxActions setup reset mkCmds = property $ do+  env <- evalIO setup+  let commands = lockstepCommands (mkCmds env)+  actions <- forAll $+    Gen.sequential (Range.linear 1 maxActions) (initialLockstepState model0) commands+  evalIO (reset env)+  executeSequential (initialLockstepState model0) actions+{-# INLINABLE lockstepPropertyWith #-}++-- | Run a parallel lockstep property test for linearizability.+--+-- Commands run in @PropertyT IO@. Use 'Hedgehog.evalIO' to lift+-- @IO@ actions inside @lsCmdExec@.+--+-- For tests that need an IO resource (the common case), use+-- 'lockstepParallelWith'.+lockstepParallel+  :: Show model+  => model+  -> Int+  -> Int+  -> [LockstepCmd (PropertyT IO) model]+  -> Property+lockstepParallel model0 maxPrefix maxBranch cmds = property $ do+  let commands = lockstepCommands cmds+  actions <- forAll $+    Gen.parallel (Range.linear 1 maxPrefix) (Range.linear 1 maxBranch)+      (initialLockstepState model0) commands+  executeParallel (initialLockstepState model0) actions+{-# INLINABLE lockstepParallel #-}++-- | Run a parallel lockstep property test with IO-based resource setup.+--+-- Like 'lockstepPropertyWith' but uses 'Gen.parallel' and 'executeParallel'+-- to test linearizability of concurrent operations.+--+-- The @IO env@ action creates the resource before generation. The reset+-- callback runs before execution (per test case). The commands must be+-- thread-safe: concurrent 'Data.IORef.modifyIORef'' is not safe, for+-- example; use 'Data.IORef.atomicModifyIORef'',+-- 'Control.Concurrent.MVar.MVar', or 'Control.Concurrent.STM.TVar' instead.+lockstepParallelWith+  :: Show model+  => model+  -> Int+  -- ^ Max actions in the sequential prefix+  -> Int+  -- ^ Max actions per parallel branch+  -> IO env+  -- ^ Create resource (runs once per test case)+  -> (env -> IO ())+  -- ^ Reset resource (runs before each execution, including shrink attempts)+  -> (env -> [LockstepCmd (PropertyT IO) model])+  -- ^ Commands using the resource+  -> Property+lockstepParallelWith model0 maxPrefix maxBranch setup reset mkCmds = property $ do+  env <- evalIO setup+  let commands = lockstepCommands (mkCmds env)+  actions <- forAll $+    Gen.parallel (Range.linear 1 maxPrefix) (Range.linear 1 maxBranch)+      (initialLockstepState model0) commands+  evalIO (reset env)+  executeParallel (initialLockstepState model0) actions+{-# INLINABLE lockstepParallelWith #-}++-- | Sequential lockstep test for commands written in an arbitrary monad+-- @m@.+--+-- The @runM@ argument is a natural transformation that lowers the user's+-- monad to @'PropertyT' 'IO'@ (the monad hedgehog's runner requires). For+-- a @'Control.Monad.Reader.ReaderT' env ('PropertyT' 'IO')@ user-monad,+-- @runM = (\\m -> 'Control.Monad.Reader.runReaderT' m env)@; for a+-- newtype around @'PropertyT' 'IO'@, it's just the unwrapper.+--+-- This is the hedgehog-lockstep analogue of @quickcheck-lockstep@'s+-- @runActions@-with-bracket pattern: write commands once in your natural+-- monad, then thread the runner separately.+lockstepPropertyM+  :: forall m model.+     (Show model, Monad m)+  => model+  -> Int+  -> (forall a. m a -> PropertyT IO a)+  -- ^ Lower the user's monad to @'PropertyT' 'IO'@+  -> [LockstepCmd m model]+  -> Property+lockstepPropertyM model0 maxActions runM cmds = property $ do+  let commands = lockstepCommands $ map (hoistLockstepCmd runM) cmds+  actions <- forAll $+    Gen.sequential (Range.linear 1 maxActions) (initialLockstepState model0) commands+  executeSequential (initialLockstepState model0) actions+{-# INLINABLE lockstepPropertyM #-}++-- | Sequential lockstep test for commands in an arbitrary monad with an+-- IO resource.+--+-- The @runM@ callback receives the live resource and a user-monad+-- computation, and lowers it to @'PropertyT' 'IO'@. For a typical+-- @'Control.Monad.Reader.ReaderT' env ('PropertyT' 'IO')@ stack with+-- environment @env@, pass @(\\env m -> 'Control.Monad.Reader.runReaderT' m env)@.+lockstepPropertyWithM+  :: forall env m model.+     (Show model, Monad m)+  => model+  -> Int+  -> IO env+  -- ^ Create resource (runs once per test case)+  -> (env -> IO ())+  -- ^ Reset resource (runs before each execution, including shrink attempts)+  -> (forall a. env -> m a -> PropertyT IO a)+  -- ^ Lower the user's monad given the resource+  -> (env -> [LockstepCmd m model])+  -- ^ Commands using the resource, in the user's monad+  -> Property+lockstepPropertyWithM model0 maxActions setup reset runM mkCmds = property $ do+  env <- evalIO setup+  let commands = lockstepCommands $ map (hoistLockstepCmd (runM env)) (mkCmds env)+  actions <- forAll $+    Gen.sequential (Range.linear 1 maxActions) (initialLockstepState model0) commands+  evalIO (reset env)+  executeSequential (initialLockstepState model0) actions+{-# INLINABLE lockstepPropertyWithM #-}++-- | Parallel lockstep test for commands in an arbitrary monad.+--+-- See 'lockstepPropertyM' for the @runM@ contract; concurrency safety+-- requirements are the same as 'lockstepParallel'.+lockstepParallelM+  :: forall m model.+     (Show model, Monad m)+  => model+  -> Int+  -> Int+  -> (forall a. m a -> PropertyT IO a)+  -> [LockstepCmd m model]+  -> Property+lockstepParallelM model0 maxPrefix maxBranch runM cmds = property $ do+  let commands = lockstepCommands $ map (hoistLockstepCmd runM) cmds+  actions <- forAll $+    Gen.parallel (Range.linear 1 maxPrefix) (Range.linear 1 maxBranch)+      (initialLockstepState model0) commands+  executeParallel (initialLockstepState model0) actions+{-# INLINABLE lockstepParallelM #-}++-- | Parallel lockstep test for commands in an arbitrary monad with an+-- IO resource.+--+-- See 'lockstepPropertyWithM' for the @runM@ contract; concurrency safety+-- requirements are the same as 'lockstepParallelWith'.+lockstepParallelWithM+  :: forall env m model.+     (Show model, Monad m)+  => model+  -> Int+  -- ^ Max actions in the sequential prefix+  -> Int+  -- ^ Max actions per parallel branch+  -> IO env+  -- ^ Create resource (runs once per test case)+  -> (env -> IO ())+  -- ^ Reset resource (runs before each execution, including shrink attempts)+  -> (forall a. env -> m a -> PropertyT IO a)+  -- ^ Lower the user's monad given the resource+  -> (env -> [LockstepCmd m model])+  -- ^ Commands using the resource, in the user's monad+  -> Property+lockstepParallelWithM model0 maxPrefix maxBranch setup reset runM mkCmds = property $ do+  env <- evalIO setup+  let commands = lockstepCommands $ map (hoistLockstepCmd (runM env)) (mkCmds env)+  actions <- forAll $+    Gen.parallel (Range.linear 1 maxPrefix) (Range.linear 1 maxBranch)+      (initialLockstepState model0) commands+  evalIO (reset env)+  executeParallel (initialLockstepState model0) actions+{-# INLINABLE lockstepParallelWithM #-}
+ src/Hedgehog/Lockstep/State.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | The lockstep state: the user's pure model alongside a model environment+-- that maps Hedgehog t'Hedgehog.Internal.State.Var's to their model-side+-- output values.+--+-- The model environment is what makes t'Hedgehog.Lockstep.GVar.GVar'+-- resolution work across the symbolic and concrete phases.+--+-- The @LockstepState@ constructor and the @ls*@ field selectors are+-- exported from this module for library internals to use; the top-level+-- 'Hedgehog.Lockstep' facade re-exports only the type and projection+-- accessors. Treat the constructor and field selectors as internal:+-- subject to change without a major version bump.+module Hedgehog.Lockstep.State+  ( LockstepState (..)+  , ModelEnv+  , SomeVar (..)+  , initialLockstepState+  , getModel+  , getEntries+  , getNextVarId+  , getLastEntry+  , varsOfType+  , insertModelResult+  , lookupModelEntry+  ) where++import Data.Dynamic (Dynamic, toDyn)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Proxy (Proxy (..))+import Data.Typeable (TypeRep, Typeable, eqT, typeRep)+import Type.Reflection ((:~:) (..))+import Data.Functor.Classes (Ord1, liftCompare)+import Hedgehog.Internal.State (Var (..), Symbolic)++-- | Existential variable key with phase-polymorphic ordering.+--+-- Internal: not exposed in the public API. The 'Ord' instance compares+-- by type first, then by phase-specific identity ('Hedgehog.Internal.State.Name'+-- for t'Hedgehog.Internal.State.Symbolic', value for+-- t'Hedgehog.Internal.State.Concrete').+data VarKey v where+  VarKey :: (Typeable a, Ord a) => !(Var a v) -> VarKey v++instance Ord1 v => Eq (VarKey v) where+  VarKey (Var v1 :: Var x v) == VarKey (Var v2 :: Var y v) =+    case eqT @x @y of+      Just Refl -> liftCompare compare v1 v2 == EQ+      Nothing   -> False++instance Ord1 v => Ord (VarKey v) where+  compare (VarKey (Var v1 :: Var x v)) (VarKey (Var v2 :: Var y v)) =+    case eqT @x @y of+      Just Refl -> liftCompare compare v1 v2+      Nothing   -> compare (typeRep (Proxy @x)) (typeRep (Proxy @y))++-- | The model environment: associates t'Hedgehog.Internal.State.Var's+-- with their model-side output values. Stored as a 'Data.Map.Strict.Map'+-- so lookups are @O(log n)@.+--+-- Opaque: construct via 'insertModelResult' and look up via+-- 'lookupModelEntry' or 'Hedgehog.Lockstep.GVar.resolveGVar'.+newtype ModelEnv v = ModelEnv (Map (VarKey v) Dynamic)++-- | An existentially-wrapped t'Hedgehog.Internal.State.Var' with its+-- type witness.+data SomeVar v where+  SomeVar :: Typeable a => !(Var a v) -> SomeVar v++-- | Lockstep state wrapping a user-defined model.+--+-- Tracks the pure model state alongside a model environment that maps+-- variables to model-side output values. This enables+-- t'Hedgehog.Lockstep.GVar.GVar' resolution during both generation and+-- execution phases, including after shrinking.+data LockstepState model v = LockstepState+  { lsModel     :: !model+  , lsNextVarId :: {-# UNPACK #-} !Int+  , lsEntries   :: !(ModelEnv v)+  , lsVars      :: !(Map TypeRep [SomeVar v])+  -- ^ Variables grouped by type, so 'varsOfType' is a single 'Map'+  -- lookup rather than a linear filter over all variables.+  , lsLastEntry :: !(Maybe Dynamic)+  -- ^ The most recently inserted model result, used by the @Ensure@+  -- callback to compare against the real output.+  }++instance Show model => Show (LockstepState model v) where+  showsPrec p st = showParen (p > 10) $+    showString "LockstepState {model = " .+    showsPrec 0 (lsModel st) .+    showString ", vars = " .+    showsPrec 0 (sum (map length (Map.elems (lsVars st)))) .+    showString "}"++-- | Create the initial lockstep state from a model value.+initialLockstepState :: model -> LockstepState model v+initialLockstepState m = LockstepState+  { lsModel     = m+  , lsNextVarId = 0+  , lsEntries   = ModelEnv Map.empty+  , lsVars      = Map.empty+  , lsLastEntry = Nothing+  }++-- | Extract the user's model state.+getModel :: LockstepState model v -> model+getModel = lsModel++-- | Extract the model environment.+getEntries :: LockstepState model v -> ModelEnv v+getEntries = lsEntries++-- | Get the next variable ID (used internally for Ensure lookup).+getNextVarId :: LockstepState model v -> Int+getNextVarId = lsNextVarId++-- | Get the most recently inserted model result, if any. Used by the+-- @Ensure@ callback to compare against the real output.+getLastEntry :: LockstepState model v -> Maybe Dynamic+getLastEntry = lsLastEntry++-- | Enumerate all variables of a given type. @O(log n)@ in the number+-- of distinct types ever inserted, plus @O(k)@ in the number of+-- matching variables.+--+-- Useful in generators to pick a variable for a+-- t'Hedgehog.Lockstep.GVar.GVar'.+varsOfType+  :: forall a model. Typeable a+  => LockstepState model Symbolic -> [Var a Symbolic]+varsOfType st =+  case Map.lookup (typeRep (Proxy @a)) (lsVars st) of+    Nothing     -> []+    Just bucket ->+      [ var+      | SomeVar (var :: Var b Symbolic) <- bucket+      , Just Refl <- [eqT @a @b]+      ]+{-# INLINABLE varsOfType #-}++-- | Look up a model result by t'Hedgehog.Internal.State.Var' identity.+-- @O(log n)@ in the size of the model environment.+lookupModelEntry+  :: forall x v. (Typeable x, Ord x, Ord1 v)+  => Var x v -> ModelEnv v -> Maybe Dynamic+lookupModelEntry var (ModelEnv m) = Map.lookup (VarKey var) m+{-# INLINABLE lookupModelEntry #-}++-- | Insert a model result into the state and register the variable.+-- Used internally by 'Hedgehog.Lockstep.Command.toLockstepCommand'.+insertModelResult+  :: forall modelOutput output model v.+     (Typeable modelOutput, Typeable output, Ord output, Ord1 v)+  => Var output v -> modelOutput -> LockstepState model v -> LockstepState model v+insertModelResult var modelOut st =+  let varId = lsNextVarId st+      dyn   = toDyn modelOut+      tyRep = typeRep (Proxy @output)+      ModelEnv entries = lsEntries st+  in st+    { lsNextVarId = varId + 1+    , lsEntries   = ModelEnv (Map.insert (VarKey var) dyn entries)+    , lsVars      = Map.insertWith (++) tyRep [SomeVar var] (lsVars st)+    , lsLastEntry = Just dyn+    }+{-# INLINABLE insertModelResult #-}
+ test/Main.hs view
@@ -0,0 +1,43 @@+module Main (main) where++import System.Exit (exitFailure, exitSuccess)+import Test.KVStore (prop_kvSequential)+import Test.HandleStore (prop_handleSequential)+import Test.BuggyCounter (prop_buggyCounterDetected)+import Test.CustomOp (prop_customOpUnit, prop_customOpIntegration)+import Test.LabelledExamples (prop_labelledExamples)+import Test.Observation (prop_observation)+import Test.OpProjections (prop_opProjections)+import Test.ParallelKV (prop_kvParallel)+import Test.PureSort (prop_pureSort)+import Test.ReaderKV (prop_readerKV)+import Test.UnitCoverage (prop_applyOp, prop_gvarLabel, prop_mapGVar, prop_mkGVarId)+import Hedgehog (check)++main :: IO ()+main = do+  ok1 <- check prop_kvSequential+  ok2 <- check prop_handleSequential+  ok3 <- check prop_kvParallel+  ok4 <- check prop_pureSort+  ok5 <- check prop_opProjections+  ok6 <- check prop_applyOp+  ok7 <- check prop_gvarLabel+  ok8 <- check prop_mkGVarId+  ok9 <- check prop_mapGVar+  ok10 <- check prop_readerKV+  ok11 <- check prop_observation+  ok12 <- check prop_labelledExamples+  ok13 <- check prop_customOpUnit+  ok14 <- check prop_customOpIntegration+  -- BuggyCounter should FAIL (model is deliberately wrong).+  -- We verify the failure is detected.+  ok15 <- check prop_buggyCounterDetected+  let bugDetected = not ok15+  putStrLn $ if bugDetected+    then "  Buggy model correctly detected"+    else "  Buggy model was NOT detected (bug in lockstep!)"+  if and [ ok1, ok2, ok3, ok4, ok5, ok6, ok7, ok8, ok9, ok10+         , ok11, ok12, ok13, ok14, bugDetected ]+    then exitSuccess+    else exitFailure
+ test/Test/BuggyCounter.hs view
@@ -0,0 +1,122 @@+module Test.BuggyCounter+  ( prop_buggyCounterDetected+  ) where++import Data.IORef (IORef, newIORef, readIORef, modifyIORef')+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- System under test: a counter that wraps at 10+-- ---------------------------------------------------------------------------++newCounter :: IO (IORef Int)+newCounter = newIORef 0++incCounter :: IORef Int -> Int -> IO Int+incCounter ref n = do+  modifyIORef' ref (+ n)+  readIORef ref++getCounter :: IORef Int -> IO Int+getCounter = readIORef++-- ---------------------------------------------------------------------------+-- BUGGY model: doesn't wrap at 10 (but the real system does... wait,+-- actually let's make the model buggy by using a wrong increment)+-- The model always increments by 1, ignoring the actual amount.+-- ---------------------------------------------------------------------------++type Model = Int++-- ---------------------------------------------------------------------------+-- Inputs+-- ---------------------------------------------------------------------------++data IncInput v = IncInput !Int+  deriving stock (Show)++instance FunctorB IncInput where bmap _ (IncInput n) = IncInput n+instance TraversableB IncInput where btraverse _ (IncInput n) = pure (IncInput n)++data GetInput v = GetInput+  deriving stock (Show)++instance FunctorB GetInput where bmap _ GetInput = GetInput+instance TraversableB GetInput where btraverse _ GetInput = pure GetInput++-- ---------------------------------------------------------------------------+-- Commands+-- ---------------------------------------------------------------------------++cmdInc :: IORef Int -> LockstepCmd (PropertyT IO) Model+cmdInc ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ IncInput <$> Gen.int (Range.linear 1 5)+  , lsCmdExec = \(IncInput n) -> evalIO $ incCounter ref n+  , lsCmdModel = \st (IncInput _n) ->+      -- BUG: model always increments by 1+      let model = getModel st+          model' = model + 1+      in (model', model')+  , lsCmdRequire = \_ _ -> True+  , lsCmdObserve = \expected actual -> expected === actual+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag = \_ _ _ -> []+  }++cmdGet :: IORef Int -> LockstepCmd (PropertyT IO) Model+cmdGet ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ pure GetInput+  , lsCmdExec = \GetInput -> evalIO $ getCounter ref+  , lsCmdModel = \st GetInput ->+      let model = getModel st+      in (model, model)+  , lsCmdRequire = \_ _ -> True+  , lsCmdObserve = \expected actual -> expected === actual+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- Property: should FAIL because the model is buggy+--+-- Shrinking expectation (manual inspection only -- not asserted, see+-- below for why):+--+-- A fresh run should shrink to a 1- or 2-action counterexample of the+-- form @[Inc n]@ or @[Inc n, Get]@ where @n >= 2@. The bug is that the+-- model increments by 1 regardless of @n@, so:+--+-- * @Inc 1@ does not surface the bug (model 0+1=1, real 0+1=1).+-- * @Inc 2@ is the smallest @n@ where model (= 1) and real (= 2)+--   diverge.+--+-- A counterexample like @[Inc 5, Inc 4, Get, Inc 3, ...]@ would mean+-- shrinking is not running, which is a real regression. We do not+-- assert that here because:+--+-- 1. Hedgehog's @check@ returns 'Bool', not the shrunk counterexample,+--    so structured access requires @Hedgehog.Internal.Runner@ APIs we+--    do not want to depend on.+-- 2. Different shrinker versions can validly produce @Inc 2@ vs+--    @Inc 3@; both are minimal in spirit.+-- 3. Parsing the rendered failure box couples the test to Hedgehog's+--    output format.+--+-- The assertion we /do/ make below is the meaningful one: the buggy+-- model is detected at all. To eyeball the shrunk shape, run:+--+-- > cabal test --test-show-details=direct+-- ---------------------------------------------------------------------------++prop_buggyCounterDetected :: Property+prop_buggyCounterDetected = withTests 200 $+  lockstepPropertyWith+    (0 :: Model)+    30+    newCounter+    (\ref -> modifyIORef' ref (const 0))+    (\ref -> [cmdInc ref, cmdGet ref])
+ test/Test/CustomOp.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE TypeApplications #-}+-- | Demonstrates that users can extend the projection vocabulary beyond+-- the built-in 'Op' GADT.+--+-- Defines @MyOp@, a user GADT that wraps the default 'Op' and adds a+-- @MyOpHead :: MyOp [a] a@ constructor for projecting the head of a list.+-- The 'InterpretOp' instance plus a 'Show' instance is all that's needed+-- to plug it into 'mkGVar' and 'mapGVar'.+--+-- The integration property runs a small lockstep test where:+--+--   * @ListOf@ produces a non-empty @[Int]@.+--   * @ReadHead@ picks a prior @ListOf@ result and reads its head via+--     @MyOpHead@.+--+-- Real and model agree on every step, demonstrating end-to-end use of a+-- custom op including substitution during shrinking.+module Test.CustomOp+  ( prop_customOpUnit+  , prop_customOpIntegration+  ) where++import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- A user-defined op that extends 'Op' with a list-head projection.+-- ---------------------------------------------------------------------------++data MyOp a b where+  MyOfOp   :: !(Op a b) -> MyOp a b+  MyOpHead :: MyOp [a] a++instance InterpretOp MyOp where+  interpretOp (MyOfOp op) x        = interpretOp op x+  interpretOp MyOpHead    []       = Nothing+  interpretOp MyOpHead    (x : _)  = Just x++instance Show (MyOp a b) where+  show (MyOfOp op) = show op+  show MyOpHead    = "head"++-- ---------------------------------------------------------------------------+-- Unit test: the new op flows through the GVar machinery.+-- ---------------------------------------------------------------------------++prop_customOpUnit :: Property+prop_customOpUnit = withTests 1 $ property $ do+  -- applyOp directly:+  applyOp (MyOpHead :: MyOp [Int] Int) [7, 9, 11]   === Just 7+  applyOp (MyOpHead :: MyOp [Int] Int) ([] :: [Int]) === Nothing+  -- via a Concrete-phase GVar, including the label:+  let v :: Var [Int] Concrete+      v  = Var (Concrete [7, 9, 11])+      gv :: GVar Int Concrete+      gv = mkGVar v (MyOpHead :: MyOp [Int] Int)+  gvarLabel gv     === "head"+  concreteGVar gv  === Just 7+  -- mapGVar with the wrapped default ops still works on the same GVar+  -- type, mixing wrapped and custom projections in one chain.+  let vPair :: Var (Int, Int) Concrete+      vPair = Var (Concrete (4, 5))+      gvPair :: GVar Int Concrete+      gvPair = mkGVar vPair (MyOfOp OpFst :: MyOp (Int, Int) Int)+  gvarLabel gvPair === "fst"+  concreteGVar gvPair === Just 4+  -- mapGVar exercised with a custom op: chain a wrapped built-in+  -- projection with the custom MyOpHead. Starting from+  -- @Either err [Int]@: project Right to land on the [Int], then take+  -- the list head.+  let vEither :: Var (Either String [Int]) Concrete+      vEither = Var (Concrete (Right [42, 43, 44]))+      gvList :: GVar [Int] Concrete+      gvList  = mkGVar vEither (MyOfOp OpRight :: MyOp (Either String [Int]) [Int])+      gvHead :: GVar Int Concrete+      gvHead  = mapGVar (MyOpHead :: MyOp [Int] Int) gvList+  gvarLabel gvHead    === "right.head"+  concreteGVar gvHead === Just 42+  -- And the failure case: the same chain on a Left short-circuits to+  -- Nothing (the wrapped OpRight projection fails before MyOpHead runs).+  let vLeft :: Var (Either String [Int]) Concrete+      vLeft = Var (Concrete (Left "boom"))+      gvHeadFail :: GVar Int Concrete+      gvHeadFail =+        mapGVar (MyOpHead :: MyOp [Int] Int)+                (mkGVar vLeft (MyOfOp OpRight :: MyOp (Either String [Int]) [Int]))+  concreteGVar gvHeadFail === Nothing++-- ---------------------------------------------------------------------------+-- Integration test: a lockstep property using MyOpHead in a real command.+-- ---------------------------------------------------------------------------++type Model = ()++data ListOfInput v = ListOfInput ![Int]+  deriving stock (Show)++instance FunctorB ListOfInput where+  bmap _ (ListOfInput xs) = ListOfInput xs+instance TraversableB ListOfInput where+  btraverse _ (ListOfInput xs) = pure (ListOfInput xs)++data ReadHeadInput v = ReadHeadInput !(GVar Int v)+  deriving stock (Show)++instance FunctorB ReadHeadInput where+  bmap f (ReadHeadInput gv) = ReadHeadInput (bmap f gv)+instance TraversableB ReadHeadInput where+  btraverse f (ReadHeadInput gv) = ReadHeadInput <$> btraverse f gv++-- The real system stores a list in an IORef; commands return either a+-- list ('ListOf') or a single Int ('ReadHead').+cmdListOf :: IORef [Int] -> LockstepCmd (PropertyT IO) Model+cmdListOf ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ do+      -- Generate at least one element so MyOpHead never legitimately fails.+      n  <- Gen.int (Range.linear 1 5)+      xs <- Gen.list (Range.singleton n) (Gen.int (Range.linear 0 100))+      pure (ListOfInput xs)+  , lsCmdExec = \(ListOfInput xs) -> evalIO (writeIORef ref xs) >> pure xs+  , lsCmdModel = \_ (ListOfInput xs) -> (xs, ())+  , lsCmdRequire    = \_ _ -> True+  , lsCmdObserve    = runObservation ObserveEq+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++cmdReadHead :: IORef [Int] -> LockstepCmd (PropertyT IO) Model+cmdReadHead ref = LockstepCmd+  { lsCmdGen = \st ->+      case varsOfType @[Int] st of+        []   -> Nothing+        vars -> Just $ do+          var <- Gen.element vars+          let gv :: GVar Int Symbolic+              gv = mkGVar var (MyOpHead :: MyOp [Int] Int)+          pure (ReadHeadInput gv)+  , lsCmdExec = \(ReadHeadInput gv) -> do+      stored <- evalIO (readIORef ref)+      case (concreteGVar gv, stored) of+        (Just n, _ : _) -> pure (Just n)+        (_,      _    ) -> pure Nothing+  , lsCmdModel = \st (ReadHeadInput gv) ->+      (resolveGVar gv (getEntries st), ())+  , lsCmdRequire    = \_ _ -> True+  , lsCmdObserve    = runObservation ObserveEq+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++prop_customOpIntegration :: Property+prop_customOpIntegration =+  lockstepPropertyWith+    ()+    20+    (newIORef [])+    (\ref -> writeIORef ref [])+    (\ref -> [cmdListOf ref, cmdReadHead ref])
+ test/Test/HandleStore.hs view
@@ -0,0 +1,287 @@+module Test.HandleStore+  ( prop_handleSequential+  ) where++import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- System under test: a mutable handle-based store+--+-- Open returns Either String (Handle, Name). Subsequent Read/Write/Close+-- must extract the Handle from a previous Open via GVar projections:+-- OpRight >>> OpFst+-- ---------------------------------------------------------------------------++type Handle = Int+type Name = String+type Content = String++data RealStore = RealStore+  { rsNextHandle :: {-# UNPACK #-} !Int+  , rsHandles    :: !(Map Handle (Name, Content))+  }++newRealStore :: IO (IORef RealStore)+newRealStore = newIORef (RealStore 0 Map.empty)++rsOpen :: IORef RealStore -> Name -> IO (Either String (Handle, Name))+rsOpen ref name = do+  st <- readIORef ref+  let inUse = any (\(n, _) -> n == name) (rsHandles st)+  if inUse+    then pure (Left ("already open: " <> name))+    else do+      let h = rsNextHandle st+      writeIORef ref st+        { rsNextHandle = h + 1+        , rsHandles = Map.insert h (name, "") (rsHandles st)+        }+      pure (Right (h, name))++rsWrite :: IORef RealStore -> Handle -> Content -> IO (Either String ())+rsWrite ref h content = do+  st <- readIORef ref+  case Map.lookup h (rsHandles st) of+    Nothing -> pure (Left "bad handle")+    Just (name, _) -> do+      writeIORef ref st { rsHandles = Map.insert h (name, content) (rsHandles st) }+      pure (Right ())++rsRead :: IORef RealStore -> Handle -> IO (Either String Content)+rsRead ref h = do+  st <- readIORef ref+  pure $ case Map.lookup h (rsHandles st) of+    Nothing           -> Left "bad handle"+    Just (_, content) -> Right content++rsClose :: IORef RealStore -> Handle -> IO (Either String ())+rsClose ref h = do+  st <- readIORef ref+  case Map.lookup h (rsHandles st) of+    Nothing -> pure (Left "bad handle")+    Just _  -> do+      writeIORef ref st { rsHandles = Map.delete h (rsHandles st) }+      pure (Right ())++-- ---------------------------------------------------------------------------+-- Model+-- ---------------------------------------------------------------------------++data Model = Model+  { mNextHandle :: !Int+  , mHandles    :: !(Map Handle (Name, Content))+  } deriving stock (Show)++initialModel :: Model+initialModel = Model 0 Map.empty++mOpen :: Model -> Name -> (Either String (Handle, Name), Model)+mOpen m name =+  let inUse = any (\(n, _) -> n == name) (mHandles m)+  in if inUse+     then (Left ("already open: " <> name), m)+     else+       let h = mNextHandle m+           m' = m { mNextHandle = h + 1+                   , mHandles = Map.insert h (name, "") (mHandles m)+                   }+       in (Right (h, name), m')++mWrite :: Model -> Handle -> Content -> (Either String (), Model)+mWrite m h content =+  case Map.lookup h (mHandles m) of+    Nothing -> (Left "bad handle", m)+    Just (name, _) ->+      (Right (), m { mHandles = Map.insert h (name, content) (mHandles m) })++mRead :: Model -> Handle -> (Either String Content, Model)+mRead m h =+  case Map.lookup h (mHandles m) of+    Nothing           -> (Left "bad handle", m)+    Just (_, content) -> (Right content, m)++mClose :: Model -> Handle -> (Either String (), Model)+mClose m h =+  case Map.lookup h (mHandles m) of+    Nothing -> (Left "bad handle", m)+    Just _  -> (Right (), m { mHandles = Map.delete h (mHandles m) })++-- ---------------------------------------------------------------------------+-- Inputs (barbies-style HKD)+-- ---------------------------------------------------------------------------++data OpenInput v = OpenInput !Name+  deriving stock (Show)++instance FunctorB OpenInput where bmap _ (OpenInput n) = OpenInput n+instance TraversableB OpenInput where btraverse _ (OpenInput n) = pure (OpenInput n)++data WriteInput v = WriteInput !(GVar Handle v) !Content+  deriving stock (Show)++instance FunctorB WriteInput where+  bmap f (WriteInput gv c) = WriteInput (bmap f gv) c+instance TraversableB WriteInput where+  btraverse f (WriteInput gv c) = (\gv' -> WriteInput gv' c) <$> btraverse f gv++data ReadInput v = ReadInput !(GVar Handle v)+  deriving stock (Show)++instance FunctorB ReadInput where+  bmap f (ReadInput gv) = ReadInput (bmap f gv)+instance TraversableB ReadInput where+  btraverse f (ReadInput gv) = ReadInput <$> btraverse f gv++data CloseInput v = CloseInput !(GVar Handle v)+  deriving stock (Show)++instance FunctorB CloseInput where+  bmap f (CloseInput gv) = CloseInput (bmap f gv)+instance TraversableB CloseInput where+  btraverse f (CloseInput gv) = CloseInput <$> btraverse f gv++-- ---------------------------------------------------------------------------+-- GVar helpers+-- ---------------------------------------------------------------------------++type OpenResult = Either String (Handle, Name)++-- | Pick a handle GVar: projects Open's result via OpRight >>> OpFst.+pickHandle :: LockstepState Model Symbolic -> Gen (GVar Handle Symbolic)+pickHandle st = do+  let vars = varsOfType @OpenResult st+  var <- Gen.element vars+  let op :: Op OpenResult Handle+      op = OpRight >>> OpFst+  pure $ mkGVar var op++resolveHandle :: Ord1 v => GVar Handle v -> LockstepState Model v -> Maybe Handle+resolveHandle gv st = resolveGVar gv (getEntries st)++-- ---------------------------------------------------------------------------+-- Commands+-- ---------------------------------------------------------------------------++genName :: Gen Name+genName = Gen.element ["alpha", "beta", "gamma"]++cmdOpen :: IORef RealStore -> LockstepCmd (PropertyT IO) Model+cmdOpen ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ OpenInput <$> genName++  , lsCmdExec = \(OpenInput name) -> evalIO $ rsOpen ref name++  , lsCmdModel = \st (OpenInput name) ->+      mOpen (getModel st) name++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \modelResult realResult ->+      fmap (const ()) modelResult === fmap (const ()) realResult++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdWrite :: IORef RealStore -> LockstepCmd (PropertyT IO) Model+cmdWrite ref = LockstepCmd+  { lsCmdGen = \st ->+      if null (varsOfType @OpenResult st)+        then Nothing+        else Just $ WriteInput <$> pickHandle st+                               <*> Gen.string (Range.linear 0 20) Gen.alpha++  , lsCmdExec = \(WriteInput gv content) ->+      case concreteGVar gv of+        Just h  -> evalIO $ rsWrite ref h content+        Nothing -> pure (Left "bad handle")++  , lsCmdModel = \st (WriteInput gv content) ->+      case resolveHandle gv st of+        Just h  -> mWrite (getModel st) h content+        Nothing -> (Left "bad handle", getModel st)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdRead :: IORef RealStore -> LockstepCmd (PropertyT IO) Model+cmdRead ref = LockstepCmd+  { lsCmdGen = \st ->+      if null (varsOfType @OpenResult st)+        then Nothing+        else Just $ ReadInput <$> pickHandle st++  , lsCmdExec = \(ReadInput gv) ->+      case concreteGVar gv of+        Just h  -> evalIO $ rsRead ref h+        Nothing -> pure (Left "bad handle")++  , lsCmdModel = \st (ReadInput gv) ->+      case resolveHandle gv st of+        Just h  -> mRead (getModel st) h+        Nothing -> (Left "bad handle", getModel st)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdClose :: IORef RealStore -> LockstepCmd (PropertyT IO) Model+cmdClose ref = LockstepCmd+  { lsCmdGen = \st ->+      if null (varsOfType @OpenResult st)+        then Nothing+        else Just $ CloseInput <$> pickHandle st++  , lsCmdExec = \(CloseInput gv) ->+      case concreteGVar gv of+        Just h  -> evalIO $ rsClose ref h+        Nothing -> pure (Left "bad handle")++  , lsCmdModel = \st (CloseInput gv) ->+      case resolveHandle gv st of+        Just h  -> mClose (getModel st) h+        Nothing -> (Left "bad handle", getModel st)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  -- System invariant: closed handles never appear in the model's open set,+  -- so the open-handle count never exceeds the next-handle counter.+  , lsCmdInvariants = \model _ ->+      assert (Map.size (mHandles model) <= mNextHandle model)++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- Property+-- ---------------------------------------------------------------------------++prop_handleSequential :: Property+prop_handleSequential =+  lockstepPropertyWith+    initialModel+    50+    newRealStore+    (\ref -> writeIORef ref (RealStore 0 Map.empty))+    (\ref -> [cmdOpen ref, cmdWrite ref, cmdRead ref, cmdClose ref])
+ test/Test/KVStore.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+module Test.KVStore+  ( prop_kvSequential+  ) where++import Data.IORef (IORef, newIORef, readIORef, modifyIORef')+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (isJust)+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- System under test: a mutable key-value store backed by IORef+-- ---------------------------------------------------------------------------++type Store = IORef (Map String Int)++newStore :: IO Store+newStore = newIORef Map.empty++putKV :: Store -> String -> Int -> IO ()+putKV ref k v = modifyIORef' ref (Map.insert k v)++getKV :: Store -> String -> IO (Maybe Int)+getKV ref k = Map.lookup k <$> readIORef ref++deleteKV :: Store -> String -> IO ()+deleteKV ref k = modifyIORef' ref (Map.delete k)++sizeKV :: Store -> IO Int+sizeKV ref = Map.size <$> readIORef ref++-- ---------------------------------------------------------------------------+-- Model: pure Map+-- ---------------------------------------------------------------------------++type Model = Map String Int++-- ---------------------------------------------------------------------------+-- Inputs (barbies-style HKD, parameterized by v)+-- ---------------------------------------------------------------------------++data PutInput v = PutInput !String !Int+  deriving stock (Show)++instance FunctorB PutInput where bmap _ (PutInput k v) = PutInput k v+instance TraversableB PutInput where btraverse _ (PutInput k v) = pure (PutInput k v)++data GetInput v = GetInput !String+  deriving stock (Show)++instance FunctorB GetInput where bmap _ (GetInput k) = GetInput k+instance TraversableB GetInput where btraverse _ (GetInput k) = pure (GetInput k)++data DeleteInput v = DeleteInput !String+  deriving stock (Show)++instance FunctorB DeleteInput where bmap _ (DeleteInput k) = DeleteInput k+instance TraversableB DeleteInput where btraverse _ (DeleteInput k) = pure (DeleteInput k)++data SizeInput v = SizeInput+  deriving stock (Show)++instance FunctorB SizeInput where bmap _ SizeInput = SizeInput+instance TraversableB SizeInput where btraverse _ SizeInput = pure SizeInput++-- ---------------------------------------------------------------------------+-- Commands+-- ---------------------------------------------------------------------------++genKey :: Gen String+genKey = Gen.element ["a", "b", "c", "d"]++genVal :: Gen Int+genVal = Gen.int (Range.linear 0 100)++cmdPut :: Store -> LockstepCmd (PropertyT IO) Model+cmdPut store = LockstepCmd+  { lsCmdGen = \_ -> Just $ PutInput <$> genKey <*> genVal++  , lsCmdExec = \(PutInput k v) -> evalIO $ putKV store k v++  , lsCmdModel = \st (PutInput k v) ->+      let model = getModel st+      in ((), Map.insert k v model)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \() () -> pure ()++  , lsCmdInvariants = \_ _ -> pure ()++  -- Demonstrate the per-step tagging hook: split Put coverage into+  -- "new key" (size grew) vs "overwrite" (size unchanged).+  , lsCmdTag = \pre post () ->+      ["Put", if Map.size post > Map.size pre then "Put new key" else "Put overwrite"]+  }++cmdGet :: Store -> LockstepCmd (PropertyT IO) Model+cmdGet store = LockstepCmd+  { lsCmdGen = \_ -> Just $ GetInput <$> genKey++  , lsCmdExec = \(GetInput k) -> evalIO $ getKV store k++  , lsCmdModel = \st (GetInput k) ->+      let model = getModel st+      in (Map.lookup k model, model)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> do+      label "Get"+      classify "Get hit"  (isJust expected)+      classify "Get miss" (not (isJust expected))+      expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdDelete :: Store -> LockstepCmd (PropertyT IO) Model+cmdDelete store = LockstepCmd+  { lsCmdGen = \st ->+      let model = getModel st+      in if Map.null model+         then Nothing+         else Just $ DeleteInput <$> Gen.element (Map.keys model)++  , lsCmdExec = \(DeleteInput k) -> evalIO $ deleteKV store k++  , lsCmdModel = \st (DeleteInput k) ->+      let model = getModel st+      in ((), Map.delete k model)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \() () -> label "Delete"++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdSize :: Store -> LockstepCmd (PropertyT IO) Model+cmdSize store = LockstepCmd+  { lsCmdGen = \_ -> Just $ pure SizeInput++  , lsCmdExec = \SizeInput -> evalIO $ sizeKV store++  , lsCmdModel = \st SizeInput ->+      let model = getModel st+      in (Map.size model, model)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> do+      label "Size"+      expected === actual++  -- System invariant: store size is never negative.+  , lsCmdInvariants = \_ size -> assert (size >= 0)++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- Property+-- ---------------------------------------------------------------------------++prop_kvSequential :: Property+prop_kvSequential = property $ do+  store <- evalIO newStore+  let cmds = lockstepCommands+        [ cmdPut store+        , cmdGet store+        , cmdDelete store+        , cmdSize store+        ]+      initial = initialLockstepState Map.empty+  actions <- forAll $+    Gen.sequential (Range.linear 1 50) initial cmds+  executeSequential initial actions
+ test/Test/LabelledExamples.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE RankNTypes #-}+module Test.LabelledExamples+  ( prop_labelledExamples+  ) where++import Data.IORef (IORef)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Set qualified as Set+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Exercises 'lockstepLabelledExamples'.+--+-- 'lockstepLabelledExamples' runs the model only (no IO), so the unused+-- 'IORef' resource here is just a placeholder so the command record+-- compiles. A property test below asserts that every tag we expect the+-- generator to hit actually appears in the collected examples.+-- ---------------------------------------------------------------------------++type Store = IORef (Map String Int)+type Model = Map String Int++data PutInput v = PutInput !String !Int+  deriving stock (Show)+instance FunctorB PutInput where bmap _ (PutInput k v) = PutInput k v+instance TraversableB PutInput where btraverse _ (PutInput k v) = pure (PutInput k v)++data DeleteInput v = DeleteInput !String+  deriving stock (Show)+instance FunctorB DeleteInput where bmap _ (DeleteInput k) = DeleteInput k+instance TraversableB DeleteInput where btraverse _ (DeleteInput k) = pure (DeleteInput k)++genKey :: Gen String+genKey = Gen.element ["a", "b"]++cmdPut :: Store -> LockstepCmd (PropertyT IO) Model+cmdPut _ = LockstepCmd+  { lsCmdGen = \_ -> Just $ PutInput <$> genKey <*> Gen.int (Range.linear 0 100)+  , lsCmdExec = \_ -> error "lsCmdExec should not run during labelledExamples"+  , lsCmdModel = \st (PutInput k v) -> ((), Map.insert k v (getModel st))+  , lsCmdRequire = \_ _ -> True+  , lsCmdObserve = \() () -> pure ()+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag = \pre post () ->+      ["Put", if Map.size post > Map.size pre then "Put new key" else "Put overwrite"]+  }++cmdDelete :: Store -> LockstepCmd (PropertyT IO) Model+cmdDelete _ = LockstepCmd+  { lsCmdGen = \st ->+      let m = getModel st+      in if Map.null m+         then Nothing+         else Just $ DeleteInput <$> Gen.element (Map.keys m)+  , lsCmdExec = \_ -> error "lsCmdExec should not run during labelledExamples"+  , lsCmdModel = \st (DeleteInput k) -> ((), Map.delete k (getModel st))+  , lsCmdRequire = \_ _ -> True+  , lsCmdObserve = \() () -> pure ()+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag = \_ _ () -> ["Delete"]+  }++-- The "store" is never actually used: we only run the model side.+dummyStore :: Store+dummyStore = error "dummyStore: should not be evaluated by lockstepLabelledExamples"++-- | Expectation: with 100 trials of up to 12 actions each, the generator+-- should certainly hit Put, Put new key, Put overwrite, and Delete.+prop_labelledExamples :: Property+prop_labelledExamples = withTests 1 . property $ do+  examples <- evalIO $+    lockstepLabelledExamples 100 12 Map.empty+      [ cmdPut dummyStore+      , cmdDelete dummyStore+      ]+  let observed = Set.fromList (Map.keys examples)+      required = Set.fromList ["Put", "Put new key", "Put overwrite", "Delete"]+      missing  = Set.difference required observed+  if Set.null missing+    then pure ()+    else do+      footnote $ "Missing tags: " <> show (Set.toList missing)+      failure
+ test/Test/Observation.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE RankNTypes #-}+module Test.Observation+  ( prop_observation+  ) where++import Data.IORef (IORef, newIORef, readIORef, writeIORef, modifyIORef')+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Exercises 'Observation' beyond plain equality.+--+-- The system under test returns @(Int, String)@ where the @String@ is a+-- formatted, human-readable version of the @Int@ ("count=42"). The+-- model ignores formatting concerns and returns @(Int, Int)@. The+-- observation projects both sides to a common @Int@ shape via+-- 'ObservePair' + 'ObserveProject' + 'ObserveEq'.+-- ---------------------------------------------------------------------------++type Counter = IORef Int++type Model = Int++newCounter :: IO Counter+newCounter = newIORef 0++resetCounter :: Counter -> IO ()+resetCounter ref = writeIORef ref 0++bump :: Counter -> Int -> IO (Int, String)+bump ref n = do+  modifyIORef' ref (+ n)+  v <- readIORef ref+  pure (v, "count=" <> show v)++-- Inputs++data BumpInput v = BumpInput !Int+  deriving stock (Show)++instance FunctorB BumpInput where bmap _ (BumpInput n) = BumpInput n+instance TraversableB BumpInput where btraverse _ (BumpInput n) = pure (BumpInput n)++-- The model returns @(Int, Int)@ (the second Int is the same as the+-- first, deliberately matching the textual count). The real output is+-- @(Int, String)@. ObservePair lets us compare the @Int@ slot directly+-- and project the formatted @String@ slot back to @Int@ before comparing.+cmdBump :: Counter -> LockstepCmd (PropertyT IO) Model+cmdBump ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ BumpInput <$> Gen.int (Range.linear 1 5)++  , lsCmdExec = \(BumpInput n) -> evalIO (bump ref n)++  , lsCmdModel = \st (BumpInput n) ->+      let v = getModel st + n+      in ((v, v), v)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve =+      runObservation $+        ObservePair+          ObserveEq+          (ObserveProject id parseCount)++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }+  where+    -- Strip "count=" prefix from the formatted string.+    parseCount :: String -> Int+    parseCount s =+      case drop (length ("count=" :: String)) s of+        digits -> read digits++prop_observation :: Property+prop_observation =+  lockstepPropertyWith+    0+    20+    newCounter+    resetCounter+    (\ref -> [cmdBump ref])
+ test/Test/OpProjections.hs view
@@ -0,0 +1,187 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+module Test.OpProjections+  ( prop_opProjections+  ) where++import Data.IORef (IORef, atomicModifyIORef', newIORef, writeIORef)+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Exercises OpSnd and OpLeft.+--+-- A 'Make' command returns @Either String (Int, Int)@: @Right (n, n*2)@ for+-- non-negative inputs, @Left "negative"@ for negative inputs. Subsequent+-- commands project out:+--+--   * the doubled value via @OpRight >>> OpSnd@   (exercises 'OpSnd')+--   * the error message via @OpLeft@              (exercises 'OpLeft')+--+-- Partial projections: when the underlying 'Either' doesn't match the+-- projection, both 'resolveGVar' (model) and 'concreteGVar' (real) should+-- return 'Nothing', and the model/real must agree.+-- ---------------------------------------------------------------------------++type MakeOutput = Either String (Int, Int)++-- | The "real system" here is just an allocation counter so that outputs+-- differ across repeated calls with the same input; this keeps the model+-- from being trivially stateless.+newRef :: IO (IORef Int)+newRef = newIORef 0++resetRef :: IORef Int -> IO ()+resetRef ref = writeIORef ref 0++data Model = Model { mCalls :: !Int }+  deriving stock (Show)++initialModel :: Model+initialModel = Model 0++-- ---------------------------------------------------------------------------+-- Inputs+-- ---------------------------------------------------------------------------++data MakeInput v = MakeInput !Int+  deriving stock (Show)++instance FunctorB MakeInput where+  bmap _ (MakeInput n) = MakeInput n++instance TraversableB MakeInput where+  btraverse _ (MakeInput n) = pure (MakeInput n)++data ReadDoubledInput v = ReadDoubledInput !(GVar Int v)+  deriving stock (Show)++instance FunctorB ReadDoubledInput where+  bmap f (ReadDoubledInput gv) = ReadDoubledInput (bmap f gv)++instance TraversableB ReadDoubledInput where+  btraverse f (ReadDoubledInput gv) = ReadDoubledInput <$> btraverse f gv++data ReadErrorInput v = ReadErrorInput !(GVar String v)+  deriving stock (Show)++instance FunctorB ReadErrorInput where+  bmap f (ReadErrorInput gv) = ReadErrorInput (bmap f gv)++instance TraversableB ReadErrorInput where+  btraverse f (ReadErrorInput gv) = ReadErrorInput <$> btraverse f gv++-- ---------------------------------------------------------------------------+-- Make: produces @Either String (Int, Int)@+-- ---------------------------------------------------------------------------++make :: IORef Int -> Int -> IO MakeOutput+make ref n = do+  _ <- atomicModifyIORef' ref (\c -> (c + 1, c + 1))+  pure $ if n >= 0+    then Right (n, n * 2)+    else Left ("negative: " <> show n)++cmdMake :: IORef Int -> LockstepCmd (PropertyT IO) Model+cmdMake ref = LockstepCmd+  { lsCmdGen = \_ -> Just $ MakeInput <$> Gen.int (Range.linear (-5) 5)++  , lsCmdExec = \(MakeInput n) -> evalIO $ make ref n++  , lsCmdModel = \st (MakeInput n) ->+      let out :: MakeOutput+          out | n >= 0    = Right (n, n * 2)+              | otherwise = Left ("negative: " <> show n)+          m' = (getModel st) { mCalls = mCalls (getModel st) + 1 }+      in (out, m')++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- ReadDoubled: picks a prior Make result, projects via OpRight >>> OpSnd+-- ---------------------------------------------------------------------------++pickDoubled :: LockstepState Model Symbolic -> Gen (GVar Int Symbolic)+pickDoubled st = do+  let vars = varsOfType @MakeOutput st+  var <- Gen.element vars+  let op :: Op MakeOutput Int+      op = OpRight >>> OpSnd+  pure (mkGVar var op)++cmdReadDoubled :: LockstepCmd (PropertyT IO) Model+cmdReadDoubled = LockstepCmd+  { lsCmdGen = \st ->+      if null (varsOfType @MakeOutput st)+        then Nothing+        else Just $ ReadDoubledInput <$> pickDoubled st++  , lsCmdExec = \(ReadDoubledInput gv) -> pure (concreteGVar gv)++  , lsCmdModel = \st (ReadDoubledInput gv) ->+      (resolveGVar gv (getEntries st), getModel st)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- ReadError: picks a prior Make result, projects via OpLeft+-- ---------------------------------------------------------------------------++pickError :: LockstepState Model Symbolic -> Gen (GVar String Symbolic)+pickError st = do+  let vars = varsOfType @MakeOutput st+  var <- Gen.element vars+  let op :: Op MakeOutput String+      op = OpLeft+  pure (mkGVar var op)++cmdReadError :: LockstepCmd (PropertyT IO) Model+cmdReadError = LockstepCmd+  { lsCmdGen = \st ->+      if null (varsOfType @MakeOutput st)+        then Nothing+        else Just $ ReadErrorInput <$> pickError st++  , lsCmdExec = \(ReadErrorInput gv) -> pure (concreteGVar gv)++  , lsCmdModel = \st (ReadErrorInput gv) ->+      (resolveGVar gv (getEntries st), getModel st)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- Property+-- ---------------------------------------------------------------------------++prop_opProjections :: Property+prop_opProjections =+  lockstepPropertyWith+    initialModel+    40+    newRef+    resetRef+    (\ref -> [cmdMake ref, cmdReadDoubled, cmdReadError])
+ test/Test/ParallelKV.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+module Test.ParallelKV+  ( prop_kvParallel+  , prop_kvParallelBuggy+  ) where++import Data.IORef (IORef, atomicModifyIORef', newIORef, readIORef, writeIORef)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Thread-safe KV store using atomicModifyIORef'+-- ---------------------------------------------------------------------------++type Store = IORef (Map String Int)++newStore :: IO Store+newStore = newIORef Map.empty++resetStore :: Store -> IO ()+resetStore ref = writeIORef ref Map.empty++-- | Atomic put. Returns the size of the store after the insert.+atomicPut :: Store -> String -> Int -> IO Int+atomicPut ref k v =+  atomicModifyIORef' ref $ \m ->+    let m' = Map.insert k v m in (m', Map.size m')++-- | Atomic get.+atomicGet :: Store -> String -> IO (Maybe Int)+atomicGet ref k = Map.lookup k <$> readIORef ref++-- | Deliberately *broken* put: reads, then writes, with no atomicity.+-- Used to verify that 'lockstepParallel' detects non-linearizable behavior.+racyPut :: Store -> String -> Int -> IO Int+racyPut ref k v = do+  m <- readIORef ref+  let m' = Map.insert k v m+  writeIORef ref m'+  pure (Map.size m')++-- ---------------------------------------------------------------------------+-- Model+-- ---------------------------------------------------------------------------++type Model = Map String Int++-- ---------------------------------------------------------------------------+-- Inputs+-- ---------------------------------------------------------------------------++data PutInput v = PutInput !String !Int+  deriving stock (Show)++instance FunctorB PutInput where bmap _ (PutInput k v) = PutInput k v+instance TraversableB PutInput where btraverse _ (PutInput k v) = pure (PutInput k v)++data GetInput v = GetInput !String+  deriving stock (Show)++instance FunctorB GetInput where bmap _ (GetInput k) = GetInput k+instance TraversableB GetInput where btraverse _ (GetInput k) = pure (GetInput k)++-- ---------------------------------------------------------------------------+-- Commands+-- ---------------------------------------------------------------------------++genKey :: Gen String+genKey = Gen.element ["a", "b", "c"]++genVal :: Gen Int+genVal = Gen.int (Range.linear 0 100)++cmdPut :: (Store -> String -> Int -> IO Int) -> Store -> LockstepCmd (PropertyT IO) Model+cmdPut putImpl store = LockstepCmd+  { lsCmdGen = \_ -> Just $ PutInput <$> genKey <*> genVal++  , lsCmdExec = \(PutInput k v) -> evalIO $ putImpl store k v++  , lsCmdModel = \st (PutInput k v) ->+      let m = Map.insert k v (getModel st)+      in (Map.size m, m)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdGet :: Store -> LockstepCmd (PropertyT IO) Model+cmdGet store = LockstepCmd+  { lsCmdGen = \_ -> Just $ GetInput <$> genKey++  , lsCmdExec = \(GetInput k) -> evalIO $ atomicGet store k++  , lsCmdModel = \st (GetInput k) ->+      let m = getModel st+      in (Map.lookup k m, m)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++-- ---------------------------------------------------------------------------+-- Properties+-- ---------------------------------------------------------------------------++-- | Parallel test with atomic operations: must pass (all executions are linearizable).+prop_kvParallel :: Property+prop_kvParallel =+  lockstepParallelWith+    Map.empty+    10  -- sequential prefix+    5   -- parallel branch length+    newStore+    resetStore+    (\ref -> [cmdPut atomicPut ref, cmdGet ref])++-- | Parallel test with a deliberately racy put: used to verify that the+-- library actually exercises concurrent execution. Not used in main tests+-- because race detection is inherently flaky; kept here for manual exploration.+prop_kvParallelBuggy :: Property+prop_kvParallelBuggy =+  lockstepParallelWith+    Map.empty+    5+    5+    newStore+    resetStore+    (\ref -> [cmdPut racyPut ref, cmdGet ref])
+ test/Test/PureSort.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE RankNTypes #-}+module Test.PureSort+  ( prop_pureSort+  ) where++import Data.List qualified as List+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Exercises 'lockstepProperty' (the no-resource variant).+--+-- Each command is independent and takes no IO state: the "real" system is+-- 'Data.List.sort' and the model is an insertion sort. Both should agree+-- on every input list.+-- ---------------------------------------------------------------------------++type Model = ()++data SortInput v = SortInput ![Int]+  deriving stock (Show)++instance FunctorB SortInput where+  bmap _ (SortInput xs) = SortInput xs++instance TraversableB SortInput where+  btraverse _ (SortInput xs) = pure (SortInput xs)++insertionSort :: [Int] -> [Int]+insertionSort = foldr insert []+  where+    insert x [] = [x]+    insert x (y : ys)+      | x <= y    = x : y : ys+      | otherwise = y : insert x ys++cmdSort :: LockstepCmd (PropertyT IO) Model+cmdSort = LockstepCmd+  { lsCmdGen = \_ ->+      Just $ SortInput <$>+        Gen.list (Range.linear 0 20) (Gen.int (Range.linear (-50) 50))++  , lsCmdExec = \(SortInput xs) -> pure (List.sort xs)++  , lsCmdModel = \_ (SortInput xs) -> (insertionSort xs, ())++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = runObservation ObserveEq++  -- System invariant: a sorted list is monotonically non-decreasing.+  , lsCmdInvariants = \_ xs ->+      assert (and (zipWith (<=) xs (drop 1 xs)))++  , lsCmdTag = \_ _ _ -> []+  }++prop_pureSort :: Property+prop_pureSort = lockstepProperty () 20 [cmdSort]
+ test/Test/ReaderKV.hs view
@@ -0,0 +1,108 @@+{-# LANGUAGE RankNTypes #-}+module Test.ReaderKV+  ( prop_readerKV+  ) where++import Control.Monad.IO.Class (liftIO)+import Control.Monad.Reader (ReaderT, ask, runReaderT)+import Data.IORef (IORef, newIORef, readIORef, modifyIORef', writeIORef)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- Exercises 'lockstepPropertyWithM': commands written in+-- @ReaderT Store (PropertyT IO)@ rather than @PropertyT IO@ directly.+-- The runner ('runReaderT') is supplied separately, so command bodies+-- read the store from the environment instead of closing over it.+-- ---------------------------------------------------------------------------++type Store = IORef (Map String Int)++type AppM = ReaderT Store (PropertyT IO)++type Model = Map String Int++newStore :: IO Store+newStore = newIORef Map.empty++resetStore :: Store -> IO ()+resetStore ref = writeIORef ref Map.empty++-- Inputs++data PutInput v = PutInput !String !Int+  deriving stock (Show)++instance FunctorB PutInput where bmap _ (PutInput k v) = PutInput k v+instance TraversableB PutInput where btraverse _ (PutInput k v) = pure (PutInput k v)++data GetInput v = GetInput !String+  deriving stock (Show)++instance FunctorB GetInput where bmap _ (GetInput k) = GetInput k+instance TraversableB GetInput where btraverse _ (GetInput k) = pure (GetInput k)++genKey :: Gen String+genKey = Gen.element ["a", "b", "c"]++genVal :: Gen Int+genVal = Gen.int (Range.linear 0 100)++-- Commands run in 'AppM'. Note: the exec functions never see a 'Store'+-- argument; they read it from the ReaderT environment. The model+-- functions are unchanged, since the model is pure.+cmdPut :: LockstepCmd AppM Model+cmdPut = LockstepCmd+  { lsCmdGen = \_ -> Just $ PutInput <$> genKey <*> genVal++  , lsCmdExec = \(PutInput k v) -> do+      ref <- ask+      liftIO $ modifyIORef' ref (Map.insert k v)++  , lsCmdModel = \st (PutInput k v) ->+      ((), Map.insert k v (getModel st))++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \() () -> pure ()++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++cmdGet :: LockstepCmd AppM Model+cmdGet = LockstepCmd+  { lsCmdGen = \_ -> Just $ GetInput <$> genKey++  , lsCmdExec = \(GetInput k) -> do+      ref <- ask+      liftIO $ Map.lookup k <$> readIORef ref++  , lsCmdModel = \st (GetInput k) ->+      let model = getModel st+      in (Map.lookup k model, model)++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()++  , lsCmdTag = \_ _ _ -> []+  }++prop_readerKV :: Property+prop_readerKV =+  lockstepPropertyWithM+    Map.empty+    50+    newStore+    resetStore+    (\store m -> runReaderT m store)+    (\_store -> [cmdPut, cmdGet])
+ test/Test/UnitCoverage.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE TypeApplications #-}+module Test.UnitCoverage+  ( prop_applyOp+  , prop_gvarLabel+  , prop_mapGVar+  , prop_mkGVarId+  ) where++import Data.IORef (IORef, newIORef, writeIORef)+import Hedgehog+import Hedgehog.Gen qualified as Gen+import Hedgehog.Range qualified as Range++import Hedgehog.Lockstep++-- ---------------------------------------------------------------------------+-- applyOp: direct unit tests for each Op constructor+-- ---------------------------------------------------------------------------++prop_applyOp :: Property+prop_applyOp = withTests 1 $ property $ do+  applyOp (OpId :: Op Int Int) 7   === Just 7+  applyOp OpFst (1 :: Int, 'a')    === Just 1+  applyOp OpSnd (1 :: Int, 'a')    === Just 'a'+  applyOp OpLeft  (Left  'x' :: Either Char Int) === Just 'x'+  applyOp OpLeft  (Right 9   :: Either Char Int) === Nothing+  applyOp OpRight (Left  'x' :: Either Char Int) === Nothing+  applyOp OpRight (Right 9   :: Either Char Int) === Just 9+  applyOp (OpRight >>> OpFst)+          (Right (1 :: Int, 'a') :: Either String (Int, Char))+    === Just 1++-- ---------------------------------------------------------------------------+-- gvarLabel: render projection chains+-- ---------------------------------------------------------------------------++prop_gvarLabel :: Property+prop_gvarLabel = withTests 1 $ property $ do+  -- Use a Concrete-phase Var so we can construct it directly. The label+  -- only depends on the projection, not on the underlying variable.+  let v :: Var (Either String (Int, Int)) Concrete+      v = Var (Concrete (Right (1, 2)))+  gvarLabel (mkGVarId v :: GVar (Either String (Int, Int)) Concrete) === "id"+  gvarLabel (mkGVar v (OpRight :: Op (Either String (Int, Int)) (Int, Int)))+    === "right"+  gvarLabel (mkGVar v ((OpRight >>> OpFst) :: Op (Either String (Int, Int)) Int))+    === "right.fst"++-- ---------------------------------------------------------------------------+-- mapGVar: composing an additional projection onto an existing GVar+--+-- Build a GVar that projects the @Right@ branch of an @Either@, then use+-- 'mapGVar' to extend it with @OpFst@ to land on the first tuple element.+-- The resulting GVar resolves to that element via 'concreteGVar' and+-- carries the composed projection in its label.+-- ---------------------------------------------------------------------------++prop_mapGVar :: Property+prop_mapGVar = withTests 1 $ property $ do+  let v :: Var (Either String (Int, Int)) Concrete+      v = Var (Concrete (Right (7, 9)))+      gvRight :: GVar (Int, Int) Concrete+      gvRight = mkGVar v (OpRight :: Op (Either String (Int, Int)) (Int, Int))+      gvFst :: GVar Int Concrete+      gvFst = mapGVar OpFst gvRight+  gvarLabel gvFst    === "right.fst"+  concreteGVar gvFst === Just 7+  -- Mapping with OpId is the identity (modulo the label suffix).+  concreteGVar (mapGVar OpId gvRight) === Just (7, 9)++-- ---------------------------------------------------------------------------+-- mkGVarId: an integration test using identity projection+--+-- The action returns a single Int. A later command takes a GVar Int that+-- references the prior result via mkGVarId (no projection). The Echo+-- command simply returns the GVar's concrete value, demonstrating that+-- mkGVarId resolves correctly across both phases.+-- ---------------------------------------------------------------------------++type Model = ()++data PutInput v = PutInput !Int+  deriving stock (Show)++instance FunctorB PutInput where bmap _ (PutInput n) = PutInput n+instance TraversableB PutInput where btraverse _ (PutInput n) = pure (PutInput n)++data EchoInput v = EchoInput !(GVar Int v)+  deriving stock (Show)++instance FunctorB EchoInput where+  bmap f (EchoInput gv) = EchoInput (bmap f gv)+instance TraversableB EchoInput where+  btraverse f (EchoInput gv) = EchoInput <$> btraverse f gv++cmdPut :: IORef Int -> LockstepCmd (PropertyT IO) Model+cmdPut ref = LockstepCmd+  { lsCmdGen        = \_ -> Just $ PutInput <$> Gen.int (Range.linear 0 100)+  , lsCmdExec       = \(PutInput n) -> evalIO (writeIORef ref n) >> pure n+  , lsCmdModel      = \_ (PutInput n) -> (n, ())+  , lsCmdRequire    = \_ _ -> True+  , lsCmdObserve    = \expected actual -> expected === actual+  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++cmdEcho :: LockstepCmd (PropertyT IO) Model+cmdEcho = LockstepCmd+  { lsCmdGen = \st ->+      case varsOfType @Int st of+        []   -> Nothing+        vars -> Just $ do+          var <- Gen.element vars+          pure $ EchoInput (mkGVarId var)++  , lsCmdExec = \(EchoInput gv) ->+      pure (concreteGVar gv)++  , lsCmdModel = \st (EchoInput gv) ->+      (resolveGVar gv (getEntries st), ())++  , lsCmdRequire = \_ _ -> True++  , lsCmdObserve = \expected actual -> expected === actual++  , lsCmdInvariants = \_ _ -> pure ()+  , lsCmdTag        = \_ _ _ -> []+  }++prop_mkGVarId :: Property+prop_mkGVarId =+  lockstepPropertyWith+    ()+    20+    (newIORef 0)+    (\ref -> writeIORef ref 0)+    (\ref -> [cmdPut ref, cmdEcho])