My hope is that using HMock will remove the need for creating a bunch of test implementations for the various custom monads for effects¹ in the projects, thereby reducing the amount of test code overall. I also suspect that it will make the tests clearer and easier to read, as the behaviour of the mocks are closer to the tests using the mocks.

When capturing the ID it's no longer possible to use a simple Map Int Text for the state, because I don't actually have the ID until I have an HTTP response. However, the ID is playing an important role in the constructing of a sequence of actions. The trick is to use Var Int v instead of an ordinary Int. As I understand it, and I believe that's a good enough understanding to make use of Hedgehog possible, is that this way the ID is an opaque blob in the construction phase, and it's turned into a concrete value during execution. When in the opaque state it implements enough type classes to be useful for my purposes.

newtype State (v :: * -> *)= State (M.Map (Var Int v) Text)
  deriving (Eq, Show)

When taking a closer look at the Callback type not all the callbacks will get the state in the same form, opaque or concrete, and one of them, Update actually receives the state in both states depending on the phase of execution. This has the most impact on the add user action. To deal with it there's a need to rearrange the code a bit, to be specific, commandExecute can no longer return a tuple of both the ID and the status of the HTTP response because the update function can't reach into the tuple, which it needs to update the state.

That means the commandExecute function will have to do tests too. It is nice to keep all tests in the callbacks, but by sticking a MonadTest m constraint on the commandExecute it turns into a nice solution anyway.

addUser :: (MonadGen n, MonadIO m, MonadTest m) => Command n m State
addUser = Command gen exec [ Update u
                           ]
  where
    gen _ = Just $ AddUser <$> Gen.text (Range.linear 0 42) Gen.alpha

    exec (AddUser n) = do
      (s, ui) <- liftIO $ do
        mgr <- newManager defaultManagerSettings
        addReq <- parseRequest "POST http://localhost:3000/users"
        let addReq' = addReq { requestBody = RequestBodyLBS (encode $ User 0 n)}
        addResp <- httpLbs addReq' mgr
        let user = decode (responseBody addResp) :: Maybe User
        return (responseStatus addResp, user)
      status201 === s
      assert $ isJust ui
      (userName <$> ui) === Just n
      return $ userId $ fromJust ui

    u (State m) (AddUser n) o = State (M.insert o n m)

I found that once I'd come around to folding the Ensure callback into the commandExecute function the rest fell out from the types.

The other actions, deleting a user and getting a user, required only minor changes and the changes were rather similar in both cases.

Not the type for the action needs to take a Var Int v instead of just a plain Int.

newtype DeleteUser (v :: * -> *) = DeleteUser (Var Int v)
  deriving (Eq, Show)

Which in turn affect the implementation of HTraversable

instance HTraversable DeleteUser where
  htraverse f (DeleteUser vi) = DeleteUser <$> htraverse f vi

Then the changes to the Command mostly comprise use of concrete in places where the real ID is needed.

deleteUser :: (MonadGen n, MonadIO m) => Command n m State
deleteUser = Command gen exec [ Update u
                              , Require r
                              , Ensure e
                              ]
  where
    gen (State m) = case M.keys m of
      [] -> Nothing
      ks -> Just $ DeleteUser <$> Gen.element ks

    exec (DeleteUser vi) = liftIO $ do
      mgr <- newManager defaultManagerSettings
      delReq <- parseRequest $ "DELETE http://localhost:3000/users/" ++ show (concrete vi)
      delResp <- httpNoBody delReq mgr
      return $ responseStatus delResp

    u (State m) (DeleteUser i) _ = State $ M.delete i m

    r (State m) (DeleteUser i) = i `elem` M.keys m

    e _ _ (DeleteUser _) r = r === status200

This post concludes my playing around with state machines in Hedgehog for this time. I certainly hope I find the time to put it to use on some larger API soon. In particular I'd love to put it to use at work; I think it'd be an excellent addition to the integration tests we currently have.

The first issue I run into is

━━━ Main ━━━
  ✗ sequential failed after 18 tests and 1 shrink.

        ┏━━ tst/test-01.hs ━━━
     89 ┃ getUser :: (MonadGen n, MonadIO m) => Command n m State
     90 ┃ getUser = Command gen exec [ Require r
     91 ┃                            , Ensure e
     92 ┃                            ]
     93 ┃   where
     94 ┃     gen (State m) = case M.keys m of
     95 ┃       [] -> Nothing
     96 ┃       ks -> Just $ GetUser <$> Gen.element ks
     97 ┃
     98 ┃     exec (GetUser i) = liftIO $ do
     99 ┃       mgr <- newManager defaultManagerSettings
    100 ┃       getReq <- parseRequest $ "GET http://localhost:3000/users/" ++ show i
    101 ┃       getResp <- httpLbs getReq mgr
    102 ┃       let us = decode $ responseBody getResp :: Maybe [User]
    103 ┃       return (status200 == responseStatus getResp, us)
    104 ┃
    105 ┃     r (State m) (GetUser i) = i `elem` M.keys m
    106 ┃
    107 ┃     e _ _ (GetUser _) (r, us) = do
    108 ┃       r === True
    109 ┃       assert $ isJust us
    110 ┃       (length <$> us) === Just 1
        ┃       ^^^^^^^^^^^^^^^^^^^^^^^^^^
        ┃       │ Failed (- lhs =/= + rhs)
        ┃       │ - Just 0
        ┃       │ + Just 1

        ┏━━ tst/test-01.hs ━━━
    118 ┃ prop_seq :: Property
    119 ┃ prop_seq = property $ do
    120 ┃   actions <- forAll $ Gen.sequential (Range.linear 1 10) initialState [addUser, deleteUser, getUser]
        ┃   │ Var 0 = AddUser ""
        ┃   │ Var 1 = GetUser 1
    121 ┃   resetWS
    122 ┃   executeSequential initialState actions

    This failure can be reproduced by running:
    > recheck (Size 17) (Seed 2158538972777046104 (-1442908127347265675)) sequential

  ✗ 1 failed.

It's easy to verify this using httpie:

$ http -p b POST :3000/users userId:=0 "userName="
{
    "userId": 0,
    "userName": ""
}
$ http -p b GET :3000/users/1
[]

It's clear that my assumption that User ID starts at 1 is wrong. Luckily fixing that isn't too difficult. Instead of defining the update function for addUser as

u (State m) (AddUser n) _o = State $ M.insert k n m
  where
    k = succ $ foldl max 0 (M.keys m)

I define it as

u (State m) (AddUser n) _o = State $ M.insert k n m
  where
    k = case M.keys m of
      [] -> 0
      ks -> succ $ foldl max 0 ks

The complete code at this point can be found here.

With that fix in place another issue with the model shows up

━━━ Main ━━━
  ✗ sequential failed after 74 tests and 2 shrinks.

        ┏━━ tst/test-01.hs ━━━
     91 ┃ getUser :: (MonadGen n, MonadIO m) => Command n m State
     92 ┃ getUser = Command gen exec [ Require r
     93 ┃                            , Ensure e
     94 ┃                            ]
     95 ┃   where
     96 ┃     gen (State m) = case M.keys m of
     97 ┃       [] -> Nothing
     98 ┃       ks -> Just $ GetUser <$> Gen.element ks
     99 ┃
    100 ┃     exec (GetUser i) = liftIO $ do
    101 ┃       mgr <- newManager defaultManagerSettings
    102 ┃       getReq <- parseRequest $ "GET http://localhost:3000/users/" ++ show i
    103 ┃       getResp <- httpLbs getReq mgr
    104 ┃       let us = decode $ responseBody getResp :: Maybe [User]
    105 ┃       return (status200 == responseStatus getResp, us)
    106 ┃
    107 ┃     r (State m) (GetUser i) = i `elem` M.keys m
    108 ┃
    109 ┃     e _ _ (GetUser _) (r, us) = do
    110 ┃       r === True
    111 ┃       assert $ isJust us
    112 ┃       (length <$> us) === Just 1
        ┃       ^^^^^^^^^^^^^^^^^^^^^^^^^^
        ┃       │ Failed (- lhs =/= + rhs)
        ┃       │ - Just 0
        ┃       │ + Just 1

        ┏━━ tst/test-01.hs ━━━
    120 ┃ prop_seq :: Property
    121 ┃ prop_seq = property $ do
    122 ┃   actions <- forAll $ Gen.sequential (Range.linear 1 10) initialState [addUser, deleteUser, getUser]
        ┃   │ Var 0 = AddUser ""
        ┃   │ Var 1 = DeleteUser 0
        ┃   │ Var 2 = AddUser ""
        ┃   │ Var 3 = GetUser 0
    123 ┃   resetWS
    124 ┃   executeSequential initialState actions

    This failure can be reproduced by running:
    > recheck (Size 73) (Seed 3813043122711576923 (-444438259649958339)) sequential

  ✗ 1 failed.

Again, verifying this using httpie shows what the issue is

$ http -p b POST :3000/users userId:=0 "userName="
{
    "userId": 0,
    "userName": ""
}
$ http -p b DELETE :3000/users/0
$ http -p b POST :3000/users userId:=0 "userName="
{
    "userId": 1,
    "userName": ""
}
$ http -p b GET :3000/users/0
[]

In other words, the model assumes that the 0 User ID get's re-used.

To fix this I need a bigger change. The central bit is that the state is changed to keep track of the index more explicitly. That is, it changes from

newtype State (v :: * -> *)= State (M.Map Int Text)
  deriving (Eq, Show)

to

data State (v :: * -> *)= State Int (M.Map Int Text)
  deriving (Eq, Show)

That change does, quite obviously, require a bunch of other changes in the other functions dealing with the state. The complete file can be viewed here.

After this the tests pass, so all is good in the world, right?

In the test I defined the property over rather short sequences of commands. What happens if I increase the (maximum) length of the sequences a bit? Instead using Range.linear 1 10 I'll use Range.linear 1 1000. Well, besides taking slightly longer to run I get another sequence of commands that triggers an issue:

━━━ Main ━━━
  ✗ sequential failed after 13 tests and 29 shrinks.

        ┏━━ tst/test-01.hs ━━━
     87 ┃ getUser :: (MonadGen n, MonadIO m) => Command n m State
     88 ┃ getUser = Command gen exec [ Require r
     89 ┃                            , Ensure e
     90 ┃                            ]
     91 ┃   where
     92 ┃     gen (State _ m) = case M.keys m of
     93 ┃       [] -> Nothing
     94 ┃       ks -> Just $ GetUser <$> Gen.element ks
     95 ┃
     96 ┃     exec (GetUser i) = liftIO $ do
     97 ┃       mgr <- newManager defaultManagerSettings
     98 ┃       getReq <- parseRequest $ "GET http://localhost:3000/users/" ++ show i
     99 ┃       getResp <- httpLbs getReq mgr
    100 ┃       let us = decode $ responseBody getResp :: Maybe [User]
    101 ┃       return (status200 == responseStatus getResp, us)
    102 ┃
    103 ┃     r (State _ m) (GetUser i) = i `elem` M.keys m
    104 ┃
    105 ┃     e _ _ (GetUser _) (r, us) = do
    106 ┃       r === True
    107 ┃       assert $ isJust us
    108 ┃       (length <$> us) === Just 1
        ┃       ^^^^^^^^^^^^^^^^^^^^^^^^^^
        ┃       │ Failed (- lhs =/= + rhs)
        ┃       │ - Just 0
        ┃       │ + Just 1

        ┏━━ tst/test-01.hs ━━━
    116 ┃ prop_seq :: Property
    117 ┃ prop_seq = property $ do
    118 ┃   actions <- forAll $ Gen.sequential (Range.linear 1 1000) initialState [addUser, deleteUser, getUser]
        ┃   │ Var 0 = AddUser ""
        ┃   │ Var 2 = AddUser ""
        ┃   │ Var 5 = AddUser ""
        ┃   │ Var 7 = AddUser ""
        ┃   │ Var 9 = AddUser ""
        ┃   │ Var 11 = AddUser ""
        ┃   │ Var 20 = AddUser ""
        ┃   │ Var 28 = AddUser ""
        ┃   │ Var 30 = AddUser ""
        ┃   │ Var 32 = AddUser ""
        ┃   │ Var 33 = AddUser ""
        ┃   │ Var 34 = AddUser ""
        ┃   │ Var 37 = AddUser ""
        ┃   │ Var 38 = AddUser ""
        ┃   │ Var 41 = AddUser ""
        ┃   │ Var 45 = AddUser ""
        ┃   │ Var 47 = GetUser 15
    119 ┃   resetWS
    120 ┃   executeSequential initialState actions

    This failure can be reproduced by running:
    > recheck (Size 12) (Seed 2976784816810995551 (-47094630645854485)) sequential

  ✗ 1 failed.

That is, after inserting 16 users, we don't see any user when trying to get that 16th user (User ID 15). That's a proper bug in the server.

As a matter of fact, this is the bug I put into the server and was hoping to find. In particular, I wanted hedgehog to find the minimal sequence leading to this bug.¹ Which it clearly has!

The API is the same as in the post on using QuickCheck, with one little difference, I've been lazy when implementing GET /users/:id and return a list of users (that makes it easy to represent a missing :id).

Just like last time I'm using as simple a model as I think I can get away with, based on the API above:

newtype State (v :: * -> *)= State (M.Map Int Text)
  deriving (Eq, Show)

initialState :: State v
initialState = State M.empty

That extra v is something that hedgehog requires. Why? I don't really know, and luckily I don't have to care to make it all work. One thing though, the language pragma KindSignatures is necessary to use that kind of syntax.

Representing an API call requires three things

1. a type
2. an implementation of HTraversable for the type
3. a function producing a Command for the type

I represent the three API calls with these three types

newtype AddUser (v :: * -> *) = AddUser Text
  deriving (Eq, Show)

newtype DeleteUser (v :: * -> *) = DeleteUser Int
  deriving (Eq, Show)

newtype GetUser (v :: * -> *) = GetUser Int
  deriving (Eq, Show)

Again that v pops up, but as with the model state, there's no need to pay any attention to it.

For the implementation of HTraversable I was greatly helped by the registry example. Their implementations are fairly straight forward, which is a good thing since the need for them is internal to hedgehog.

instance HTraversable AddUser where
  htraverse _ (AddUser n) = AddUser <$> pure n

instance HTraversable DeleteUser where
  htraverse _ (DeleteUser i) = DeleteUser <$> pure i

instance HTraversable GetUser where
  htraverse _ (GetUser i) = GetUser <$> pure i

Once these two things are out of the way we get to the meat of the implementation of the API calls, a function creating a Command instance for each type of API call. The exact type for all three functions will be

(MonadGen n, MonadIO m) => Command n m State

which doesn't say a whole lot, I think. After reading the documentation I found it a little clearer, but the two examples, state machine testing and registry, was what cleared things up for me.¹ In an attempt at being overly explicit I wrote these functions in the same style. This is what it ended up looking like for the AddUser type:

addUser :: (MonadGen n, MonadIO m) => Command n m State
addUser = Command gen exec [ Update u
                           , Ensure e
                           ]
  where
    gen _ = Just $ AddUser <$> Gen.text (Range.linear 0 42) Gen.alpha

    exec (AddUser n) = liftIO $ do
      mgr <- newManager defaultManagerSettings
      addReq <- parseRequest "POST http://localhost:3000/users"
      let addReq' = addReq { requestBody = RequestBodyLBS (encode $ User 0 n)}
      addResp <- httpLbs addReq' mgr
      let user = decode (responseBody addResp) :: Maybe User
      return (responseStatus addResp, user)

    u (State m) (AddUser n) _o = State $ M.insert k n m
      where
        k = succ $ foldl max 0 (M.keys m)

    e _ _ (AddUser n) (r, ui) = do
      r === status201
      assert $ isJust ui
      (userName <$> ui) === Just n

Piece by piece:

1. gen is the generator of data. It takes one argument, the current state, but for AddUser I have no use for it. The user name is generated using a generator for Text, and rather arbitrarily I limit the names to 42 characters.
2. exec is the action that calls the web service. Here I'm using http-client to make the call and aeson to parse the response into a User. It produces output.
3. u is a function for updating the model state. It's given the current state, the command and the output. All I need to to do for AddUser is to pick a userId and associate it with the generated name.
4. e is a function for checking post-conditions, in other words checking properties that must hold after exec has run and the state has been updated. It's given four arguments, the previous state, the updated state, the command and the output. The tests here are on the HTTP response code and the returned user name. I think that will do for the time being.

The function for DeleteUser follows the same pattern

deleteUser :: (MonadGen n, MonadIO m) => Command n m State
deleteUser = Command gen exec [ Update u
                              , Require r
                              , Ensure e
                              ]
  where
    gen (State m) = case M.keys m of
      [] -> Nothing
      ks -> Just $ DeleteUser <$> Gen.element ks

    exec (DeleteUser i) = liftIO $ do
      mgr <- newManager defaultManagerSettings
      delReq <- parseRequest $ "DELETE http://localhost:3000/users/" ++ show i
      delResp <- httpNoBody delReq mgr
      return $ responseStatus delResp

    u (State m) (DeleteUser i) _ = State $ M.delete i m

    r (State m) (DeleteUser i) = i `elem` M.keys m

    e _ _ (DeleteUser _) r = r === status200

I think only two pieces need further explanation:

1. gen only returns a DeleteUser with an index actually present in the model state. If there are no users in the model then Nothing is returned. As far as I understand that means that generated programs will only make calls to delete existing users.²
2. r is a pre-condition that programs only delete users that exist. At first I had skipped this pre-condition, thinking that it'd be enough to have gen only create delete calls for existing users. However, after reading the documentation of Command and Callback a bit more closely I realised that I might need a pre-condition to make sure that this holds true also while shrinking.

The final function, for GetUser requires no further explanation so I only present it here

getUser :: (MonadGen n, MonadIO m) => Command n m State
getUser = Command gen exec [ Require r
                           , Ensure e
                           ]
  where
    gen (State m) = case M.keys m of
      [] -> Nothing
      ks -> Just $ GetUser <$> Gen.element ks

    exec (GetUser i) = liftIO $ do
      mgr <- newManager defaultManagerSettings
      getReq <- parseRequest $ "GET http://localhost:3000/users/" ++ show i
      getResp <- httpLbs getReq mgr
      let us = decode $ responseBody getResp :: Maybe [User]
      return (status200 == responseStatus getResp, us)

    r (State m) (GetUser i) = i `elem` M.keys m

    e _ _ (GetUser _) (r, us) = do
      r === True
      assert $ isJust us
      (length <$> us) === Just 1

It looks like there are two obvious top-level properties

1. the web service works as expected when all calls are made one at a time (sequential), and
2. the web service works as expected when all calls are made in parallel.

Hedgehog provides two pairs of functions for this

1. a sequential generator with executeSequential, and
2. a parallel generator with executeParallel.

I started with the former only

prop_seq :: Property
prop_seq = property $ do
  actions <- forAll $ Gen.sequential (Range.linear 1 10) initialState [addUser, deleteUser, getUser]
  resetWS
  executeSequential initialState actions

This first creates a generator of programs of at most length 10³, then turning that into a Sequential which can be passed to executeSequential to turn into a Property.

The function resetWS clears out the web service to make sure that the tests start with a clean slate each time. Its definition is

resetWS :: MonadIO m => m ()
resetWS = liftIO $ do
  mgr <- newManager defaultManagerSettings
  resetReq <- parseRequest "POST http://localhost:3000/reset"
  void $ httpNoBody resetReq mgr

The final bit is the main function, which I wrote like this

main :: IO ()
main = do
  res <- checkSequential $ Group "Main" [("sequential", prop_seq)]
  unless res exitFailure

That is, first run the property sequentially (checkSequential) and if that fails exit with failure.

When running the test fails and gives me a program that breaks the property, and exactly what fails:

━━━ Main ━━━
  ✗ sequential failed after 13 tests and 1 shrink.

        ┏━━ tst/test-01.hs ━━━
     89 ┃ getUser :: (MonadGen n, MonadIO m) => Command n m State
     90 ┃ getUser = Command gen exec [ Require r
     91 ┃                            , Ensure e
     92 ┃                            ]
     93 ┃   where
     94 ┃     gen (State m) = case M.keys m of
     95 ┃       [] -> Nothing
     96 ┃       ks -> Just $ GetUser <$> Gen.element ks
     97 ┃
     98 ┃     exec (GetUser i) = liftIO $ do
     99 ┃       mgr <- newManager defaultManagerSettings
    100 ┃       getReq <- parseRequest $ "GET http://localhost:3000/users/" ++ show i
    101 ┃       getResp <- httpLbs getReq mgr
    102 ┃       let us = decode $ responseBody getResp :: Maybe [User]
    103 ┃       return (status200 == responseStatus getResp, us)
    104 ┃
    105 ┃     r (State m) (GetUser i) = i `elem` M.keys m
    106 ┃
    107 ┃     e _ _ (GetUser _) (r, us) = do
    108 ┃       r === True
    109 ┃       assert $ isJust us
    110 ┃       (length <$> us) === Just 1
        ┃       ^^^^^^^^^^^^^^^^^^^^^^^^^^
        ┃       │ Failed (- lhs =/= + rhs)
        ┃       │ - Just 0
        ┃       │ + Just 1

        ┏━━ tst/test-01.hs ━━━
    118 ┃ prop_seq :: Property
    119 ┃ prop_seq = property $ do
    120 ┃   actions <- forAll $ Gen.sequential (Range.linear 1 10) initialState [addUser, deleteUser, getUser]
        ┃   │ Var 0 = AddUser ""
        ┃   │ Var 1 = GetUser 1
    121 ┃   resetWS
    122 ┃   executeSequential initialState actions

    This failure can be reproduced by running:
    > recheck (Size 12) (Seed 6041776208714975061 (-2279196309322888437)) sequential

  ✗ 1 failed.

My goodness, that is pretty output!

Anyway, I'd say that the failing program has been shrunk to be minimal so I'd say that all in all this is a big step up from what I had earlier. Sure, using the hedgehog state machine API is slightly involved, but once worked out I find it fairly straight-forward and it most likely is written by people much more knowledgable than me and better than anything I could produce. Having to use generators explicitly (the hedgehog way) is neither easier nor more complicated than defining a few type class instances (the QuickCheck way). Finally, the integrated shrinking is rather brilliant and not having to implement that myself is definitely a big benefit.

Now I only have to fix the errors in the web service that the test reveal. This post is already rather long, so I'll keep that for a future post.

Many C APIs are rather stateful beasts so to test it I

1. generate a sequence of API calls (a program of sorts),
2. run the sequence against a model,
3. run the sequence against the real implementation, and
4. compare the model against the real state each step of the way.

To begin with I hacked up a simple implementation of a stack in C. The "specification" is

/**
 * Create a stack.
 */
void *create();

/**
 * Push a value onto an existing stack.
 */
void push (void *, int);

/**
 * Pop a value off an existing stack.
 */
int pop(void *);

Using inline-c to create bindings for it is amazingly simple:

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

module CApi
    where

import qualified Language.C.Inline as C
import Foreign.Ptr

C.include "stack.h"

create :: IO (Ptr ())
create = [C.exp| void * { create() } |]

push :: Ptr () -> C.CInt -> IO ()
push s i = [C.exp| void { push($(void *s), $(int i)) } |]

pop :: Ptr () -> IO C.CInt
pop s = [C.exp| int { pop($(void *s)) } |]

In the code below I import this module qualified.

To represent a sequence of calls I first used a custom type, but later realised that there really was no reason at all to not use a wrapped list:

newtype Program a = P [a]
    deriving (Eq, Foldable, Functor, Show, Traversable)

Then each of the C API functions can be represented with

data Statement = Create | Push Int | Pop
    deriving (Eq, Show)

My implementation of Arbitrary for Statement is very simple:

instance Arbitrary Statement where
    arbitrary = oneof [return Create, return Pop, liftM Push arbitrary]
    shrink (Push i) = Push <$> shrink i
    shrink _ = []

That is, arbitrary just returns one of the constructors of Statement, and shrinking only returns anything for the one constructor that takes an argument, Push.

I want to ensure that all Program Statement are valid, which means I need to define the model for running the program and functions for checking the precondition of a statement as well as for updating the model (i.e. for running the Statement).

Based on the C API above it seems necessary to track creation, the contents of the stack, and even if it isn't explicitly mentioned it's probably a good idea to track the popped value. Using record (Record is imported as R, and Record.Lens as RL) I defined it like this:

type ModelContext = [R.r| { created :: Bool, pop :: Maybe Int, stack :: [Int] } |]

Based on the rather informal specification I coded the pre-conditions for the three statements as

preCond :: ModelContext -> Statement -> Bool
preCond ctx Create = not $ RL.view [R.l| created |] ctx
preCond ctx (Push _) = RL.view [R.l| created |] ctx
preCond ctx Pop = RL.view [R.l| created |] ctx

That is

• Create requires that the stack hasn't been created already.
• Push i requires that the stack has been created.
• Pop also requires that the stack has been created.

Furthermore the "specification" suggests the following definition of a function for running a statement:

modelRunStatement :: ModelContext -> Statement -> ModelContext
modelRunStatement ctx Create = RL.set [R.l| created |] True ctx
modelRunStatement ctx (Push i) = RL.over [R.l| stack |] (i :) ctx
modelRunStatement ctx Pop = [R.r| { created = c, pop = headMay s, stack = tail s } |]
    where
        c = RL.view [R.l| created |] ctx
        s = RL.view [R.l| stack |] ctx

(This definition assumes that the model satisfies the pre-conditions, as can be seen in the use of tail.)

With this in place I can define Arbitrary for Program Statement as follows.

instance Arbitrary (Program Statement) where
    arbitrary = liftM P $ ar baseModelCtx
        where
            ar m = do
                push <- liftM Push arbitrary
                let possible = filter (preCond m) [Create, Pop, push]
                if null possible
                    then return []
                    else do
                        s <- oneof (map return possible)
                        let m' = modelRunStatement m s
                        frequency [(499, liftM2 (:) (return s) (ar m')), (1, return [])]

The idea is to, in each step, choose a valid statement given the provided model and cons it with the result of a recursive call with an updated model. The constant 499 is just an arbitrary one I chose after running arbitrary a few times to see how long the generated programs were.

For shrinking I take advantage of the already existing implementation for lists:

shrink (P p) = filter allowed $ map P (shrink p)
    where
        allowed = and . snd . mapAccumL go baseModelCtx
            where
                go ctx s = (modelRunStatement ctx s, preCond ctx s)

I would love making an implementation of Arbitrary s, where s is something that implements a type class that contains preCond, modelRunStatement and anything else needed. I made an attempt using something like

class S a where
    type Ctx a :: *

    baseCtx :: Ctx a
    preCond :: Ctx a -> a -> Bool
    ...

However, when trying to use baseCtx in an implementation of arbitrary I ran into the issue of injectivity. I'm still not entirely sure what that means, or if there is something I can do to work around it. Hopefully someone reading this can offer a solution.

When running the sequence of Statement against the C code I catch the results in

type RealContext = [r| { o :: Ptr (), pop :: Maybe Int } |]

Actually running a statement and capturing the output in a RealContext is easily done using inline-c and record:

realRunStatement :: RealContext -> Statement -> IO RealContext
realRunStatement ctx Create = CApi.create >>= \ ptr -> return $ RL.set [R.l| o |] ptr ctx
realRunStatement ctx (Push i) = CApi.push o (toEnum i) >> return ctx
    where
        o = RL.view [R.l| o |] ctx
realRunStatement ctx Pop = CApi.pop o >>= \ v -> return $ RL.set [R.l| pop |] (Just (fromEnum v)) ctx
    where
        o = RL.view [R.l| o |] ctx

Comparing a ModelContext and a RealContext is easily done:

compCtx :: ModelContext -> RealContext -> Bool
compCtx mc rc = mcC == rcC && mcP == rcP
    where
        mcC = RL.view [R.l| created |] mc
        rcC = RL.view [R.l| o |] rc /= nullPtr
        mcP = RL.view [R.l| pop|] mc
        rcP = RL.view [R.l| pop|] rc

With all that in place I can finally write a function for checking the validity of a program:

validProgram :: Program Statement -> IO Bool
validProgram p = and <$> snd <$> mapAccumM go (baseModelCtx, baseRealContext) p
    where
        runSingleStatement mc rc s = realRunStatement rc s >>= \ rc' -> return (modelRunStatement mc s, rc')

        go (mc, rc) s = do
            ctxs@(mc', rc') <- runSingleStatement mc rc s
            return (ctxs, compCtx mc' rc')

(This uses mapAccumM from an earlier post of mine.)

To wrap this all up I then define the property

prop_program :: Program Statement -> Property
prop_program p = monadicIO $ run (validProgram p) >>= assert

and a main function

main :: IO ()
main = quickCheck prop_program

Edit 2015-07-17: Adjusted the description of the pre-conditions to match the code.