diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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). diff --git a/hedgehog-lockstep.cabal b/hedgehog-lockstep.cabal new file mode 100644 --- /dev/null +++ b/hedgehog-lockstep.cabal @@ -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 diff --git a/src/Hedgehog/Lockstep.hs b/src/Hedgehog/Lockstep.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep.hs @@ -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 diff --git a/src/Hedgehog/Lockstep/Command.hs b/src/Hedgehog/Lockstep/Command.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/Command.hs @@ -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 #-} diff --git a/src/Hedgehog/Lockstep/Examples.hs b/src/Hedgehog/Lockstep/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/Examples.hs @@ -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)) diff --git a/src/Hedgehog/Lockstep/GVar.hs b/src/Hedgehog/Lockstep/GVar.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/GVar.hs @@ -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 diff --git a/src/Hedgehog/Lockstep/Observe.hs b/src/Hedgehog/Lockstep/Observe.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/Observe.hs @@ -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 #-} diff --git a/src/Hedgehog/Lockstep/Op.hs b/src/Hedgehog/Lockstep/Op.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/Op.hs @@ -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 #-} diff --git a/src/Hedgehog/Lockstep/Property.hs b/src/Hedgehog/Lockstep/Property.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/Property.hs @@ -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 #-} diff --git a/src/Hedgehog/Lockstep/State.hs b/src/Hedgehog/Lockstep/State.hs new file mode 100644 --- /dev/null +++ b/src/Hedgehog/Lockstep/State.hs @@ -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 #-} diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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 diff --git a/test/Test/BuggyCounter.hs b/test/Test/BuggyCounter.hs new file mode 100644 --- /dev/null +++ b/test/Test/BuggyCounter.hs @@ -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]) diff --git a/test/Test/CustomOp.hs b/test/Test/CustomOp.hs new file mode 100644 --- /dev/null +++ b/test/Test/CustomOp.hs @@ -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]) diff --git a/test/Test/HandleStore.hs b/test/Test/HandleStore.hs new file mode 100644 --- /dev/null +++ b/test/Test/HandleStore.hs @@ -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]) diff --git a/test/Test/KVStore.hs b/test/Test/KVStore.hs new file mode 100644 --- /dev/null +++ b/test/Test/KVStore.hs @@ -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 diff --git a/test/Test/LabelledExamples.hs b/test/Test/LabelledExamples.hs new file mode 100644 --- /dev/null +++ b/test/Test/LabelledExamples.hs @@ -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 diff --git a/test/Test/Observation.hs b/test/Test/Observation.hs new file mode 100644 --- /dev/null +++ b/test/Test/Observation.hs @@ -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]) diff --git a/test/Test/OpProjections.hs b/test/Test/OpProjections.hs new file mode 100644 --- /dev/null +++ b/test/Test/OpProjections.hs @@ -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]) diff --git a/test/Test/ParallelKV.hs b/test/Test/ParallelKV.hs new file mode 100644 --- /dev/null +++ b/test/Test/ParallelKV.hs @@ -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]) diff --git a/test/Test/PureSort.hs b/test/Test/PureSort.hs new file mode 100644 --- /dev/null +++ b/test/Test/PureSort.hs @@ -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] diff --git a/test/Test/ReaderKV.hs b/test/Test/ReaderKV.hs new file mode 100644 --- /dev/null +++ b/test/Test/ReaderKV.hs @@ -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]) diff --git a/test/Test/UnitCoverage.hs b/test/Test/UnitCoverage.hs new file mode 100644 --- /dev/null +++ b/test/Test/UnitCoverage.hs @@ -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])