diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Xavier Shay (c) 2018
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Author name here nor the names of other
+      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
+OWNER 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,126 @@
+# Dovin
+
+A proof assistant for [Possibility
+Storm](http://www.possibilitystorm.com/)-style Magic: The Gathering puzzles.
+
+> He has an innate talent, heightened by magic, that allows him to clearly see
+> the flaws in any system or machine. After mere moments of scrutiny, Dovin can
+> provide a complete analysis, noting a particular machine's weaknesses,
+> highlighting its shortcomings, and predicting with startling accuracy exactly
+> how and when it will fail. --- [Dovin Baan, Planeswalker](https://magic.wizards.com/en/story/planeswalkers/dovin-baan)
+
+It provides a haskell DSL for expressing Magic actions, with tracking of life
+and other counters and validation of pre- and post- conditions. For example, if
+you try to tap a permanent that is already tapped, it will error. Or if you try
+to target a creature with hexproof. It can also track state-based effects, such
+as "all creatures get +1/+1" or "other creatures gain hexproof".
+
+It does not try to provide a full ruleset implementation, instead it's more
+akin to letting you lay out cards and counters in front of you and manipulate
+them as you would in a real game of paper magic.
+
+I've only added actions "as needed" to solve problems, so the built-in
+functions are rather incomplete right now. It is straightforward to add more
+though. See `src/Dovin/V2.hs` in conjuction with `src/Dovin/Actions.hs` for
+supported and tested actions, and `src/Dovin/Dump.hs` for untested experimental
+ones.
+
+## Example
+
+``` haskell
+module Solutions.Example where
+
+import Dovin.V2
+
+main = run formatter solution
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 3
+
+    withLocation Hand $ addInstant "Plummet"
+    withLocation Play $ do
+      addLands 2 "Forest"
+
+    as Opponent $ do
+      withLocation Play $ do
+        withAttributes [flying, token] $ addCreature (4, 4) "Angel"
+        withAttributes [flying]
+          $ withEffect
+              matchInPlay
+              (matchOtherCreatures <> (const $ matchAttribute creature))
+              (pure . setAttribute hexproof)
+          $ addCreature (3, 4) "Shalai, Voice of Plenty"
+
+  step "Plummet to destroy Shalai" $ do
+    tapForMana "G" (numbered 1 "Forest")
+    tapForMana "G" (numbered 2 "Forest")
+    cast "1G" "Plummet"
+    resolve "Plummet"
+    with "Shalai, Voice of Plenty" $ \enemy -> do
+      target enemy
+      validate (matchAttribute flying) enemy
+      destroy enemy
+
+formatter :: Int -> Formatter
+formatter 2 = manaFormatter
+  <> cardFormatter "opponent creatures" (matchLocation (Opponent, Play))
+formatter _ = boardFormatter
+
+manaFormatter = attributeFormatter $ do
+  attribute "availble mana" $
+    countCards (matchAttribute land <> missingAttribute tapped)
+```
+
+`run` uses the supplied formatter to print out the board state at each step:
+
+    1. Initial state
+          (Active,Hand):
+            Plummet (instant)
+          (Active,Play):
+            Forest 1 (land)
+            Forest 2 (land)
+          (Opponent,Play):
+            Angel (creature,flying,hexproof,token) (4/4, 0)
+            Shalai, Voice of Plenty (creature,flying) (3/4, 0)
+    2. Plummet to destroy Shalai
+          availble mana: 0
+          opponent creatures:
+            Angel (creature,flying,token) (4/4, 0)
+
+## Solutions Index
+
+See `src/Solutions` for more extensive usage (spoiler alert: these are
+solutions for published Possibility Storm puzzles!)
+
+* `Dominaria5` uses a planeswalker.
+* `RivalsOfIxalan7` uses `withEffect` to model `exert`
+  effects, and shows how to verify multiple blocking scenarios.
+* `Core19_9` has a fancy formatter to correctly track how much
+  mana is available when working with `Powerstone Shard`, as well as spell
+  tracking for `Aetherflux Reservoir`.
+* `GuildsOfRavnicaPre2` uses `forCards` to model undergrowth
+  for a `Rhizome Lurcher`.
+* `GuildsOfRavnica1` uses `mentor`.
+* `GuildsOfRavnica3` uses a sacrifice wrapper to repeatedly
+  create treasure tokens.
+* `GuildsOfRavnica8` shows using counters to correctly track
+  `Muldrotha, the Gravetide` usage.
+* `GuildsOfRavnica9` handles `storm`.
+* `ExplorersOfIxalanContest` handles some pretty weird damage
+  interactions.
+* `UltimateMasters` shows how to track opponent actions.
+
+## Development
+
+    bin/dev  # Launch an interactive REPL
+    bin/test # Runs all tests and lints
+    bin/run  # Runs all solutions
+
+`src/Dovin/Dump.hs` is currently a dumping ground for prototype code. Actions
+are in the process of being moved to `Dovin.Actions`. To be moved they must:
+
+  * Be unit tested.
+  * Be documented.
+  * The primary target card of an action should be the final parameter.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,74 @@
+import Control.Arrow
+import Control.Monad (filterM)
+import Data.Char
+import Data.List
+import Data.Ord
+import Distribution.Simple
+import Distribution.Simple.Utils
+import Distribution.Verbosity
+import System.Directory
+  ( doesDirectoryExist
+  , doesFileExist
+  , getDirectoryContents
+  )
+import System.FilePath hiding (combine)
+
+-- A pre-build hook to automatically generate Solutions.all, an array
+-- containing all solutions in `src/Solutions`.
+main = defaultMainWithHooks simpleUserHooks
+  { buildHook = \pkg lbi hooks flags -> do
+     writeAllSolutions
+     buildHook simpleUserHooks pkg lbi hooks flags
+  }
+
+toModuleName x = intercalate "." . ("Solutions":) . splitDirectories . dropExtension $ x
+
+writeAllSolutions :: IO ()
+writeAllSolutions = do
+  modules <- map toModuleName <$> getFilesRecursive "src/Solutions"
+  let header = "module Solutions where"
+
+  let imports = unlines . map ("import qualified " <>) $ modules
+
+  let array = "all = [\n  " <> (intercalate ",\n  " . map formatSolution $ modules) <> "\n  ]"
+
+  let contents = unlines [header, imports, array]
+  rewriteFileEx normal "src/Solutions.hs" contents
+
+  where
+    formatSolution m = "("
+      <> show (drop (length "Solutions.") m) <> ", "
+      <> m <> ".solution, "
+      <> m <> ".formatter)"
+
+-- All these functions copy+pasted from hspec-discover
+getFilesRecursive :: FilePath -> IO [FilePath]
+getFilesRecursive baseDir = sortNaturally <$> go []
+
+  where
+    go :: FilePath -> IO [FilePath]
+    go dir = do
+      c <- map (dir </>) . filter (`notElem` [".", ".."]) <$> getDirectoryContents (baseDir </> dir)
+      dirs <- filterM (doesDirectoryExist . (baseDir </>)) c >>= mapM go
+      files <- filterM (doesFileExist . (baseDir </>)) c
+      return (files ++ concat dirs)
+
+sortNaturally :: [String] -> [String]
+sortNaturally = sortBy (comparing naturalSortKey)
+
+data NaturalSortKey = NaturalSortKey [Chunk]
+  deriving (Eq, Ord)
+
+data Chunk = Numeric Integer Int | Textual [(Char, Char)]
+  deriving (Eq, Ord)
+
+naturalSortKey :: String -> NaturalSortKey
+naturalSortKey = NaturalSortKey . chunks
+  where
+    chunks [] = []
+    chunks s@(c:_)
+      | isDigit c = Numeric (read num) (length num) : chunks afterNum
+      | otherwise = Textual (map (toLower &&& id) str) : chunks afterStr
+      where
+        (num, afterNum) = span  isDigit s
+        (str, afterStr) = break isDigit s
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,14 @@
+module Main where
+
+import Control.Monad (forM_)
+import Dovin
+
+import qualified Solutions
+
+main :: IO ()
+--main = run formatter solution
+main = runAll
+
+runAll =
+  forM_ Solutions.all $ \(name, solution, formatter) ->
+    run formatter solution
diff --git a/dovin.cabal b/dovin.cabal
new file mode 100644
--- /dev/null
+++ b/dovin.cabal
@@ -0,0 +1,132 @@
+cabal-version: 1.24
+
+-- This file has been generated from package.yaml by hpack version 0.31.1.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 64287929507673044e7103b8e99c63a3a57295a03eadbdd2273ea38a6655949d
+
+name:           dovin
+version:        0.1.0.0
+synopsis:       A proof assistant for Magic: The Gathering puzzles.
+description:    Please see the README on GitHub at <https://github.com/githubuser/dovin#readme>
+category:       Games
+homepage:       https://github.com/xaviershay/dovin#readme
+bug-reports:    https://github.com/xaviershay/dovin/issues
+author:         Xavier Shay
+maintainer:     contact@xaviershay.com
+copyright:      2018 Xavier Shay
+license:        BSD3
+license-file:   LICENSE
+build-type:     Custom
+extra-source-files:
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/xaviershay/dovin
+
+custom-setup
+  setup-depends:
+      Cabal
+    , base >=4.7 && <5
+    , directory
+    , filepath
+
+library
+  exposed-modules:
+      Dovin
+      Dovin.Actions
+      Dovin.Attributes
+      Dovin.Builder
+      Dovin.Dump
+      Dovin.Formatting
+      Dovin.Helpers
+      Dovin.Monad
+      Dovin.Prelude
+      Dovin.Types
+      Dovin.V1
+      Dovin.V2
+      Lib
+      Solutions
+      Solutions.Channel
+      Solutions.Core19_9
+      Solutions.Dominaria5
+      Solutions.Example
+      Solutions.ExplorersOfIxalanContest
+      Solutions.GuildsOfRavnica1
+      Solutions.GuildsOfRavnica3
+      Solutions.GuildsOfRavnica8
+      Solutions.GuildsOfRavnica9
+      Solutions.GuildsOfRavnicaPre2
+      Solutions.RivalsOfIxalan7
+      Solutions.UltimateMasters
+  other-modules:
+      Paths_dovin
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , hashable
+    , lens
+    , mtl
+    , parsec
+    , unordered-containers
+  default-language: Haskell2010
+
+executable dovin
+  main-is: Main.hs
+  other-modules:
+      Paths_dovin
+  hs-source-dirs:
+      app
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , dovin
+    , hashable
+    , lens
+    , mtl
+    , parsec
+    , unordered-containers
+  default-language: Haskell2010
+
+test-suite dovin-test
+  type: exitcode-stdio-1.0
+  main-is: Driver.hs
+  other-modules:
+      Activate
+      Counter
+      Damage
+      Discard
+      Exert
+      Flashback
+      Jumpstart
+      Move
+      Resolve
+      Spec
+      StateBasedActions
+      TestPrelude
+      TestPrelude.V2
+      TestSolutions
+      Trigger
+      Paths_dovin
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wunused-imports
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , dovin
+    , hashable
+    , lens
+    , mtl
+    , parsec
+    , tasty
+    , tasty-discover
+    , tasty-hunit
+    , tasty-quickcheck
+    , unordered-containers
+  default-language: Haskell2010
diff --git a/src/Dovin.hs b/src/Dovin.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin.hs
@@ -0,0 +1,5 @@
+module Dovin
+  ( module Dovin.V2
+  ) where
+
+import Dovin.V2
diff --git a/src/Dovin/Actions.hs b/src/Dovin/Actions.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Actions.hs
@@ -0,0 +1,939 @@
+{-|
+Actions correspond to things you can do in Magic. They progress the state
+machine while verifying applicable properties. The all run inside a
+'GameMonad'.
+
+Actions will modify the state as specified by the effects listed in their
+documentation. If any of the validation steps fail away, the proof will fail.
+Actions are /not/ atomic: if one fails, some effects may have already been
+applied.
+-}
+module Dovin.Actions (
+  step
+  -- * Casting
+  , cast
+  , castFromLocation
+  , counter
+  , flashback
+  , jumpstart
+  , resolve
+  , resolveTop
+  , splice
+  , tapForMana
+  -- * Uncategorized
+  , activate
+  , attackWith
+  , combatDamage
+  , damage
+  , discard
+  , exert
+  , moveTo
+  , transitionTo
+  , transitionToForced
+  , trigger
+  -- * Validations
+  , validate
+  , validateCanCastSorcery
+  , validateLife
+  , validatePhase
+  , validateRemoved
+  -- * State-based Actions
+  -- | Fine-grained control over when state-based actions are run. By default,
+  -- all actions will 'runStateBasedEffects' on completion, so most of the time
+  -- you don't need to use these functions explicitly.
+  , runStateBasedActions
+  , withStateBasedActions
+  -- * Low-level
+  -- | These actions provide low-level control over the game. Where possible,
+  -- try to use the more descriptive higher-level actions.
+  , addMana
+  , move
+  , remove
+  , spendMana
+  , tap
+  , untap
+  ) where
+
+import           Dovin.Attributes
+import           Dovin.Helpers
+import           Dovin.Prelude
+import           Dovin.Types
+import           Dovin.Builder
+import Dovin.Monad
+
+import qualified Data.HashMap.Strict as M
+import Data.Maybe (listToMaybe)
+import qualified Data.List
+
+import Control.Arrow (second)
+import Control.Monad.Reader (local)
+import Control.Monad.State
+import Control.Monad.Writer
+import Control.Lens
+
+action :: String -> GameMonad () -> GameMonad ()
+action name m = m
+
+-- | Add mana to actor's mana pool.
+--
+-- > addMana "2RG"
+--
+-- [Validates]:
+--
+--   * Mana specification is valid.
+--
+-- [Effects]:
+--
+--   * Mana pool is increased.
+addMana :: ManaString -> GameMonad ()
+addMana amount = do
+  p <- view envActor
+
+  modifying
+    (manaPoolFor p)
+    (parseMana amount <>)
+
+-- | Casts a card from actor's hand. See 'castFromLocation' for specification.
+--
+-- > cast "R" "Shock"
+--
+-- [Validates]:
+--
+--   * Card exists in hand.
+cast :: ManaPool -> CardName -> GameMonad ()
+cast mana cn = do
+  actor <- view envActor
+  castFromLocation (actor, Hand) mana cn
+
+-- | Move a card to the stack, spending the specified mana. If not tracking
+-- mana, use the empty string to cast for no mana. Typically you will want to
+-- 'resolve' after casting. For the common case of casting from hand, see
+-- 'cast'. See 'spendMana' for additional mana validations and effects.
+--
+-- > castFromLocation "1B" "Oathsworn Vampire" >> resolveTop
+--
+-- [Validates]:
+--
+--   * Card exists in location.
+--   * If not an instant or has flash, see 'validateCanCastSorcery` for extra
+--     validations.
+--
+-- [Effects]:
+--
+--   * Card moved to top of stack.
+--   * Counter 'storm' incremented if card has 'instant' or 'sorcery'
+--     attribute.
+castFromLocation :: CardLocation -> ManaPool -> CardName -> GameMonad ()
+castFromLocation loc mana name = action "castFromLocation" $ do
+  card <- requireCard name mempty
+
+  validate (matchLocation loc) name
+  unless
+    (hasAttribute instant card || hasAttribute flash card)
+    validateCanCastSorcery
+
+  modifyCard name (location . _2) $ const Stack
+
+  card <- requireCard name mempty
+
+  spendMana mana
+
+  when
+    (hasAttribute sorcery card || hasAttribute instant card) $
+    modifying
+      (counters . at storm . non 0)
+      (+ 1)
+
+  modifying
+    stack
+    ((:) name)
+
+-- | Remove a spell from the stack.
+--
+-- > counter "Shock"
+--
+-- [Validates]
+--
+--   * Card is on stack.
+--   * Card is not a triggered or activated ability.
+--
+-- [Effects]
+--
+--   * Card is moved to graveyard. (See 'move' for alternate effects.)
+counter :: CardName -> GameMonad ()
+counter expectedName = do
+  actor <- view envActor
+  c <- requireCard expectedName $
+            labelMatch "on stack" (matchLocation (actor, Stack))
+         <> invert (          matchAttribute triggered
+                    `matchOr` matchAttribute activated)
+
+  moveTo Graveyard expectedName
+
+  modifying
+    stack
+    (Data.List.delete expectedName)
+
+-- | Cast a card from actor's graveyard, exiling it when it leaves
+-- the stack. See 'castFromLocation' for further specification.
+--
+-- > flashback "R" "Shock"
+--
+-- Does not validate whether the card actually has a flashback cost. If
+-- important, use a wrapper function in your solution:
+--
+-- @
+-- flashbackSnapped mana castName = do
+--   validate (matchAttribute "snapcastered") castName
+--   flashback mana castName
+-- @
+--
+-- [Validates]
+--
+--   * Card is in actor's graveyard.
+--
+-- [Effects]
+--
+--   * Card gains 'exileWhenLeaveStack'.
+flashback :: ManaPool -> CardName -> GameMonad ()
+flashback mana castName = do
+  actor <- view envActor
+  spendMana mana
+  castFromLocation (actor, Graveyard) "" castName
+  gainAttribute exileWhenLeaveStack castName
+
+-- | Cast a card from active player's graveyard, discarding a card in
+-- addition to its mana cost, exiling it when it leaves the stack. See
+-- 'castFromLocation' for further specification.
+--
+-- > jumpstart "R" "Mountain" "Shock"
+--
+-- [Validates]
+--
+--   * Card is in actor's graveyard.
+--   * Discard card is in actor's hand.
+--
+-- [Effects]
+--
+--   * Card gains 'exileWhenLeaveStack'.
+--   * Discard card moved to graveyard.
+jumpstart :: ManaPool -> CardName -> CardName -> GameMonad ()
+jumpstart mana discardName castName = do
+  actor <- view envActor
+  spendMana mana
+  discard discardName
+  castFromLocation (actor, Graveyard) "" castName
+  gainAttribute exileWhenLeaveStack castName
+
+-- | Resolves a card on the stack.
+--
+-- > cast "R" "Shock" >> resolve "Shock"
+--
+-- [Validates]
+--
+--     * Stack is not empty.
+--     * Card is on top of stack.
+--
+-- [Effects]
+--
+--     * See 'resolveTop'.
+resolve :: CardName -> GameMonad ()
+resolve expectedName = do
+  s <- use stack
+
+  case s of
+    [] -> throwError $ "stack is empty, expecting " <> expectedName
+    (name:ss) -> do
+      unless (name == expectedName) $
+        throwError $ "unexpected top of stack: expected "
+                       <> expectedName
+                       <> ", got "
+                       <> name
+
+      resolveTop
+
+
+-- | Resolves the top card of the stack. Use this for simple cast-and-resolve
+-- scenarios. For more complicated stack states, prefer 'resolve' with a named
+-- spell to ensure the expected one is resolving.
+--
+-- [Validates]
+--
+--     * Stack is not empty.
+--
+-- [Effects]
+--
+--     * If spell, move card to graveyard of owner.
+--     * If permanent, move card to play area of owner.
+--     * If trigger, remove card.
+--     * See 'move' for possible alternate effects, depending on card
+--       attributes.
+resolveTop :: GameMonad ()
+resolveTop = action "resolveTop" $ do
+  s <- use stack
+
+  case s of
+    []     -> throwError "stack is empty"
+    (x:xs) -> do
+      c <- requireCard x mempty
+
+      if hasAttribute instant c || hasAttribute sorcery c then
+        moveTo Graveyard x
+      else if hasAttribute triggered c || hasAttribute activated c then
+        remove x
+      else
+        moveTo Play x
+
+      assign stack xs
+
+-- | Splices a spell on to a previously cast arcane spell.
+--
+-- > splice "Goryo's Vengeance" "2RR" "Through the Breach"
+--
+-- [Validates]
+--
+--   * Target spell is arcane.
+--   * Target spell is on stack.
+--   * Spliced spell is in hand.
+--   * See 'spendMana' for additional validations.
+--
+-- [Effects]
+--
+--   * See 'spendMana' for additional effects.
+splice :: CardName -> ManaString -> CardName -> GameMonad ()
+splice target cost name = action "splice" $ do
+  actor <- view envActor
+
+  validate (matchAttribute arcane) target
+  validate (matchLocation (actor, Stack)) target
+    `catchError` const (throwError $ target <> " not on stack")
+  validate (matchLocation (actor, Hand)) name
+    `catchError` const (throwError $ name <> " not in hand")
+  spendMana cost
+
+-- | Combination of 'tap' and 'addMana', see them for specification.
+tapForMana :: ManaString -> CardName -> GameMonad ()
+tapForMana amount name = do
+  tap name
+  addMana amount
+
+-- | Transition to a new game phase or step.
+--
+-- > transitionTo DeclareAttackers
+--
+-- [Validates]
+--
+--   * The new phase would occur after the current phase in a normal turn.
+--
+-- [Effects]
+--
+--   * Empty the mana pool.
+--   * Transition to new phase.
+transitionTo :: Phase -> GameMonad ()
+transitionTo newPhase = do
+  actual <- use phase
+
+  when (newPhase <= actual) $
+    throwError $ "phase "
+      <> show newPhase
+      <> " does not occur after "
+      <> show actual
+
+  transitionToForced newPhase
+
+-- | Equivalent to 'transitionTo' except it skips all validation. Useful when
+-- an effect has modified the normal order of phases, such as adding an extra
+-- combat step.
+transitionToForced :: Phase -> GameMonad ()
+transitionToForced newPhase = do
+  assign manaPool mempty
+  assign phase newPhase
+
+-- | Triggers an effect of a permanent. Typically you will want to `resolve`
+-- after triggering.
+--
+-- > activate "Draw Card" "Dawn of Hope" >> resolveTop
+--
+-- [Validates]
+--
+--   * Card is in play or graveyard.
+--   * Card is cotrolled by actor.
+--
+-- [Effects]
+--
+--   * A card with 'triggered' is added to stack.
+trigger :: CardName -> CardName -> GameMonad ()
+trigger triggerName sourceName = do
+  actor <- view envActor
+  card <-
+    requireCard
+      sourceName
+      (  matchController actor
+      <> labelMatch "in play or graveyard" (
+           matchLocation (actor, Play)
+           `matchOr`
+           matchLocation (actor, Graveyard)
+         )
+      )
+
+  withLocation Stack $ withAttribute triggered $ addCard triggerName
+
+  modifying
+    stack
+    ((:) triggerName)
+
+
+-- | Move a card from one location to another.
+--
+-- > move (Opponent, Play) (Active, Play) "Angel"
+--
+-- [Validates]:
+--
+--     * Card exists in source location.
+--     * Destination is not stack (use a 'cast' variant instead).
+--     * Destination does not match source.
+--     * If card has 'token' attribute, source is in play. (Removing token once
+--       they have left play is handled by 'runStateBasedActions'.)
+--     * If card has 'copy' attribute, source is the stack. (Removing token
+--       once they have left play is handled by 'runStateBasedActions'.)
+--
+-- [Effects]:
+--
+--     * Card moved to destination location.
+--     * If card is leaving play, remove all damage, counters, and gained
+--       attributes.
+--     * If card has 'exileWhenLeaveStack' attribute, move to exile and remove
+--       'exileWhenLeaveStack' instead.
+--     * If card has 'undying', is moving from play to graveyard, and has no
+--       +1\/+1 counters, add a +1\/+1 counter instead. (Note: undying should
+--       move card to graveyard then back to play for owner, but since neither
+--       triggers nor owner tracking are implemented, this simplification is
+--       valid.)
+--     * If card is entering play or changing controller, add 'summoned'
+--       attribute.
+move :: CardLocation -> CardLocation -> CardName -> GameMonad ()
+move from to name = action "move" $ do
+  c <- requireCard name $ matchLocation from
+
+  when (from == to) $
+    throwError "cannot move to same location"
+
+  when (snd to == Stack) $
+    throwError "cannot move directly to stack"
+
+  when (hasAttribute token c && snd from /= Play) $
+    throwError "cannot move token from non-play location"
+
+  when (hasAttribute copy c && snd from /= Stack) $
+    throwError "cannot move copy from non-stack location"
+
+  when (snd from == Stack) $
+    modifying stack (filter (/= name))
+
+  when (snd to == Play) $
+    gainAttribute summoned name
+
+  when (snd from == Play && snd to /= Play) $ do
+    modifyCard name cardPlusOneCounters (const 0)
+    modifyCard name cardDamage (const 0)
+    modifyCard name cardAttributes (const $ view cardDefaultAttributes c)
+
+  -- These conditionals are acting on the card state _before_ any of the above
+  -- changes were applied.
+  if hasAttribute exileWhenLeaveStack c then
+    do
+      loseAttribute exileWhenLeaveStack name
+      moveTo Exile name
+  else if snd from == Play && snd to == Graveyard && view cardPlusOneCounters c == 0 && hasAttribute undying c then
+    modifyCard name cardPlusOneCounters (+ 1)
+  else
+    modifyCard name location (const to)
+
+-- | Activate an ability of a permanent. See 'spendMana' for additional mana
+-- validations and effects. Typically you will want to `resolve` after
+-- activating.
+--
+-- > activate "Create Soldier" "3W" "Dawn of Hope" >> resolveTop
+--
+-- [Validates]
+--
+--   * Card is in play or graveyard.
+--   * Card is cotrolled by actor.
+--
+-- [Effects]
+--
+--   * A card with 'activated' is added to stack.
+activate :: CardName -> ManaPool -> CardName -> GameMonad ()
+activate stackName mana targetName = do
+  actor <- view envActor
+  card <-
+    requireCard
+      targetName
+      (  matchController actor
+      <> labelMatch "in play or graveyard" (
+           matchLocation (actor, Play)
+           `matchOr`
+           matchLocation (actor, Graveyard)
+         )
+      )
+
+  spendMana mana
+
+  withLocation Stack $ withAttribute activated $ addCard stackName
+
+  modifying
+    stack
+    ((:) stackName)
+
+-- | Start an attack with the given creatures.
+--
+-- > attackWith ["Fanatical Firebrand"]
+--
+-- [Validates]
+--
+--   * Cards are in play.
+--   * Cards have 'creature' attribute.
+--   * Cards either have 'haste' or are missing 'summoned'.
+--
+-- [Effects]
+--
+--   * Cards become tapped, unless they have 'vigilance'.
+--   * Cards gain 'attacking' attribute.
+--   * Transitions to 'DeclareAttackers' step.
+attackWith :: [CardName] -> GameMonad ()
+attackWith cs = do
+  transitionTo DeclareAttackers
+
+  forM_ cs $ \cn -> do
+    c <- requireCard cn
+           (matchInPlay
+             <> matchAttribute "creature"
+             <> labelMatch "does not have summoning sickness" (
+                    matchAttribute haste
+                    `matchOr`
+                    missingAttribute summoned
+                ))
+    forCards
+      (matchName cn <> missingAttribute vigilance)
+      tap
+    gainAttribute attacking cn
+
+-- | Apply combat damage between an attacker and blockers, using a simple
+-- damage assignment algorithm. For more complex assignments, use 'damage'
+-- directly.
+--
+-- > combatDamage ["Spirit 1", "Spirit 2"] "Angel"
+--
+-- See 'damage' for other validations and effects.
+--
+-- [Validates]
+--
+--   * Attacker has attribute 'attacking'.
+--   * Attacker and blockers are in play.
+--   * Attacker controlled by current actor.
+--   * Blockers have attribute 'creature'.
+--
+-- [Effects]
+--
+--   * Damage is dealt to blockers in order given, with the final blocker
+--     receiving any left over damage.
+--   * If no blockers, damage is dealt to opposing player.
+--   * If attacker has 'trample', any remaining damage is dealt to opposing
+--     player.
+combatDamage :: [CardName] -> CardName -> GameMonad ()
+combatDamage blockerNames attackerName = do
+  actor <- view envActor
+  attacker <- requireCard attackerName
+    $ matchInPlay <> matchAttribute attacking <> matchController actor
+
+  blockers <-
+    mapM
+      (\cn -> requireCard cn $ matchInPlay <> matchAttribute creature)
+      blockerNames
+
+  let power = view cardPower attacker
+
+  rem <- foldM (folder attacker) power blockers
+
+  if hasAttribute trample attacker || null blockers then
+    -- Assign leftover damage to opponent
+    damage (const rem) (targetPlayer . opposing $ actor) attackerName
+  else
+    -- Assign any leftover damage to final blocker
+    maybe
+      (return ())
+      (\x -> damage
+               (const rem)
+               (targetCard . view cardName $ x)
+               attackerName
+      )
+      (listToMaybe . reverse $ blockers)
+
+  where
+    folder attacker rem blocker = do
+      let blockerName      = view cardName blocker
+      let blockerPower     = view cardPower blocker
+      let blockerToughness = view cardToughness blocker
+      let attackPower = minimum [blockerToughness, rem]
+
+      damage
+        (const attackPower)
+        (targetCard blockerName)
+        attackerName
+
+      damage
+        (const blockerPower)
+        (targetCard attackerName)
+        blockerName
+
+      return $ rem - attackPower
+
+-- | Applies damage from a source to a target.
+--
+-- > damage (const 2) (targetPlayer Opponent) "Shock"
+--
+-- [Validates]
+--
+--   * Source exists.
+--   * Damage is not less than zero.
+--   * If targeting a card, target is in play and is either a creature or a
+--     planeswalker.
+--
+-- [Effects]
+--
+--   * Adds damage to the target.
+--   * If target is a planeswalker, remove loyalty counters instead.
+--   * If source has 'deathtouch' and target is a creature and damage is
+--     non-zero, add 'deathtouched'
+--     attribute to target.
+--   * If source has 'lifelink', controller of source gains life equal to
+--     damage dealt.
+--   * Note 'runStateBasedActions' handles actual destruction (if applicable)
+--     of creatures and planeswalkers.
+damage ::
+     (Card -> Int) -- ^ A function that returns the amount of damage to apply,
+                   -- given the source card.
+  -> Target
+  -> CardName
+  -> GameMonad ()
+damage f t source = action "damage" $ do
+  c <- requireCard source mempty
+
+  let dmg = f c
+
+  when (dmg < 0) $
+    throwError $ "damage must be positive, was " <> show dmg
+
+  damage' dmg t c
+
+  when (hasAttribute lifelink c) $
+    modifying (life . at (fst . view location $ c) . non 0) (+ dmg)
+
+  where
+    damage' dmg (TargetPlayer t) c =
+      modifying
+        (life . at t . non 0)
+        (\x -> x - dmg)
+
+    damage' dmg (TargetCard tn) c = do
+      t <- requireCard tn $ matchInPlay <>
+             (matchAttribute creature `matchOr` matchAttribute planeswalker)
+
+      when (hasAttribute creature t) $ do
+        modifyCard tn cardDamage (+ dmg)
+
+        when (dmg > 0 && hasAttribute deathtouch c) $
+          gainAttribute deathtouched tn
+
+      when (hasAttribute planeswalker t) $
+        modifyCard tn cardLoyalty (\x -> x - dmg)
+
+-- | Discard a card from the active player's hand.
+--
+-- > discard "Mountain"
+--
+-- [Validates]
+--
+--   * Card exists in active player's hand.
+--
+-- [Effects]
+--
+--   * Card moved to graveyard.
+discard :: CardName -> GameMonad ()
+discard cn = do
+  actor <- view envActor
+  move (actor, Hand) (actor, Graveyard) cn
+
+-- | Exert a card. Works best when card has an associated effect that applies
+-- when 'exerted' attribute is present.
+--
+-- > withAttributes [flying]
+-- >   $ withEffect
+-- >       (matchInPlay <> matchAttribute exerted)
+-- >       (    matchLocation . view cardLocation
+-- >         <> const (matchAttribute creature)
+-- >       )
+-- >       (pure . over cardStrength (mkStrength (1, 1) <>))
+-- >   $ addCreature (2, 2) "Tah-Crop Elite"
+-- > attackWith ["Tah-Crop Elite"]
+-- > exert "Tah-Crop Elite"
+--
+-- [Validates]
+--
+--   * Card has 'tapped' attribute.
+--
+-- [Effects]
+--
+--   * Card gains 'exerted' attribute.
+exert :: CardName -> GameMonad ()
+exert cn = do
+  validate (matchAttribute tapped) cn
+  gainAttribute exerted cn
+
+-- | Move card to location with same controller.
+--
+-- > moveTo Graveyard "Forest"
+--
+-- [Validates]:
+--
+--     * Card exists.
+--
+-- [Effects]:
+--
+--     * Card is moved to location.
+--     * See 'move' for possible alternate effects, depending on card
+moveTo :: Location -> CardName -> GameMonad ()
+moveTo dest cn = do
+  c <- requireCard cn mempty
+
+  let location = view cardLocation c
+
+  move location (second (const dest) location) cn
+
+remove :: CardName -> GameMonad ()
+remove cn = do
+  modifying cards (M.delete cn)
+  modifying stack (filter (/= cn))
+
+-- | Remove mana from the pool. Colored mana will be removed first, then extra
+-- mana of any type will be removed to match the colorless required.
+--
+-- > spendMana "2RG"
+--
+-- [Validates]:
+--
+--     * Mana specification is valid.
+--     * Sufficient mana exists in pool.
+--
+-- [Effects]:
+--
+--     * Mana pool is reduced.
+spendMana :: ManaString -> GameMonad ()
+spendMana amount =
+  forM_ (parseMana amount) $ \mana -> do
+    actor <- view envActor
+    pool <- use $ manaPoolFor actor
+    if mana == 'X' && (not . null $ pool) || mana `elem` pool then
+      modifying
+        (manaPoolFor actor)
+        (deleteFirst (if mana == 'X' then const True else (==) mana))
+    else
+      throwError $ "Mana pool (" <> pool <> ") does not contain (" <> [mana] <> ")"
+  where
+
+    -- https://stackoverflow.com/questions/14688716/removing-the-first-instance-of-x-from-a-list
+    deleteFirst _ [] = []
+    deleteFirst f (b:bc) | f b    = bc
+                         | otherwise = b : deleteFirst f bc
+
+
+-- | Taps a card.
+--
+-- [Validates]:
+--
+--   * Card is in play.
+--   * Card is not tapped.
+--
+-- [Effects]:
+--
+--   * Card gains tapped attribute.
+tap :: CardName -> GameMonad ()
+tap name = do
+  validate (matchInPlay <> missingAttribute tapped) name
+
+  gainAttribute tapped name
+
+-- | Untaps a card.
+--
+-- [Validates]:
+--
+--   * Card is in play.
+--   * Card is tapped.
+--
+-- [Effects]:
+--
+--   * Card loses tapped attribute.
+untap :: CardName -> GameMonad ()
+untap name = do
+  validate (matchInPlay <> matchAttribute tapped) name
+
+  loseAttribute tapped name
+
+-- | Validate that a card matches a matcher.
+--
+-- > validate (matchAttribute "pirate") "Angrath's Marauders"
+--
+-- [Validates]
+--
+--     * Card matches matcher.
+validate :: CardMatcher -> CardName -> GameMonad ()
+validate reqs targetName = do
+  _ <- requireCard targetName reqs
+  return ()
+
+-- | Validates that a card is no longer present in the game. Particularly
+-- helpful for checking destruction of tokens.
+--
+-- > validateRemoved "Angel"
+--
+-- [Validates]
+--
+--     * Name does not refer to a card.
+validateRemoved :: CardName -> GameMonad ()
+validateRemoved targetName = do
+  card <- use $ cards . at targetName
+  case card of
+    Nothing -> return ()
+    Just _ -> throwError $ "Card should be removed: " <> targetName
+
+-- | Validates that the game is in a particular phase.
+--
+-- > validatePhase BeginCombat
+--
+-- [Validates]
+--
+--     * Game is in the given phase.
+validatePhase :: Phase -> GameMonad ()
+validatePhase expected = do
+  actual <- use phase
+
+  when (actual /= expected) $
+    throwError $ "phase was "
+      <> show actual
+      <> ", expected "
+      <> show expected
+
+-- | Validates that a sorcery is able to be cast.
+--
+-- [Validates]
+--
+--     * Stack is empty.
+--     * In a main phase.
+validateCanCastSorcery :: GameMonad ()
+validateCanCastSorcery = do
+  validatePhase FirstMain
+    `catchError` const (validatePhase SecondMain)
+    `catchError` const (throwError "not in a main phase")
+
+  s <- use stack
+
+  unless (null s) $ throwError "stack is not empty"
+
+-- | Validates a player has a specific life total.
+--
+-- > validateLife 0 Opponent
+--
+-- [Validates]
+--
+--     * Player life equals amount.
+validateLife :: Int -> Player -> GameMonad ()
+validateLife n player = do
+  current <- use (life . at player . non 0)
+
+  when (current /= n) $
+    throwError $ show player
+      <> " life was "
+      <> show current
+      <> ", expected "
+      <> show n
+
+-- | Pause running of state-based actions for the duration of the action,
+-- running them at the end.
+withStateBasedActions :: GameMonad () -> GameMonad ()
+withStateBasedActions m = do
+  local (set envSBAEnabled False) m
+  runStateBasedActions
+
+-- | Run state-based actions. These include:
+--
+--     * If a creature does not have 'indestructible', and has damage exceeding
+--       toughess or 'deathtouched' attribute, destroy it.
+--     * If a card is a 'token' and is not in play, remove it.
+--     * If a card is a 'copy' and is not on the stack, remove it.
+--
+-- These are run implicitly at the end of each 'step', so it's not usually
+-- needed to call this explicitly. Even then, using 'withStateBasedActions' is
+-- usually preferred.
+--
+-- Running state-based actions can in turn trigger more state-based actions.
+-- This method loops until no more are generated, which has the potential for
+-- non-termination for pathological game states.
+runStateBasedActions :: GameMonad ()
+runStateBasedActions = do
+  enabled <- view envSBAEnabled
+  when enabled $
+    local (set envSBAEnabled False) runStateBasedActions'
+
+  where
+    sbaCounter :: Control.Lens.Lens' Board Int
+    sbaCounter = counters . at "sba-counter" . non 0
+
+    runStateBasedActions' = do
+      assign sbaCounter 0
+
+      let incrementCounter = modifying sbaCounter (+ 1)
+
+      forCards mempty $ \cn -> do
+        c <- requireCard cn mempty
+
+        when (applyMatcher (matchInPlay <> matchAttribute creature) c) $ do
+          let dmg = view cardDamage c
+          let toughness = view cardToughness c
+
+          unless (hasAttribute indestructible c) $
+            when (dmg >= toughness || hasAttribute deathtouched c) $
+              moveTo Graveyard cn >> incrementCounter
+
+        when (applyMatcher (invert matchInPlay) c) $
+          when (hasAttribute token c) $
+            remove cn >> incrementCounter
+
+        let matchStack =
+                       matchLocation (Active, Stack)
+             `matchOr` matchLocation (Opponent, Stack)
+
+        when (applyMatcher (invert matchStack) c) $
+          when (hasAttribute copy c) $
+            remove cn >> incrementCounter
+
+      n <- use sbaCounter
+
+      when (n > 0) runStateBasedActions'
+
+-- | Define a high-level step in the proof. A proof typically consists on
+-- multiple steps. Each step is a human-readable description, then a definition
+-- of that step using actions. If a step fails, no subsequent steps will be
+-- run.  'runStateBasedActions' is implicitly called at the end of each step.
+-- Nested 'step' invocations execute the nested action but have no other
+-- effects - generally they should be avoided.
+step :: String -> GameMonad () -> GameMonad ()
+step desc m = withStateBasedActions $ do
+  b <- get
+  let (e, b', _) = runMonad b m
+
+  tell [(desc, b')]
+  put b'
+
+  case e of
+    Left x -> throwError x
+    Right _ -> return ()
diff --git a/src/Dovin/Attributes.hs b/src/Dovin/Attributes.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Attributes.hs
@@ -0,0 +1,78 @@
+-- | Attributes with special meaning to Dovin. Use these rather than strings to
+-- avoid typos. They should generally match Magic keywords.
+module Dovin.Attributes where
+
+import Data.Monoid ((<>))
+
+import Dovin.Types
+
+-- | Return a card name suffixed by the given number.
+numbered :: Int -> CardName -> CardName
+numbered n name = name <> " " <> show n
+
+activated :: CardAttribute
+activated = "activated"
+arcane :: CardAttribute
+arcane = "arcane"
+attacking :: CardAttribute
+attacking = "attacking"
+aura :: CardAttribute
+aura = "aura"
+artifact :: CardAttribute
+artifact = "artifact"
+copy :: CardAttribute
+copy = "copy"
+creature :: CardAttribute
+creature = "creature"
+deathtouch :: CardAttribute
+deathtouch = "deathtouch"
+deathtouched :: CardAttribute
+deathtouched = "deathtouched"
+doublestrike :: CardAttribute
+doublestrike = "doublestrike"
+enchantment :: CardAttribute
+enchantment = "enchantment"
+exerted :: CardAttribute
+exerted = "exerted"
+exileWhenLeaveStack :: CardAttribute
+exileWhenLeaveStack = "exile-when-leave-stack"
+firststrike :: CardAttribute
+firststrike = "firststrike"
+flash :: CardAttribute
+flash = "flash"
+flying :: CardAttribute
+flying = "flying"
+haste :: CardAttribute
+haste = "haste"
+indestructible :: CardAttribute
+indestructible = "indestructible"
+instant :: CardAttribute
+instant = "instant"
+hexproof :: CardAttribute
+hexproof = "hexproof"
+land :: CardAttribute
+land = "land"
+legendary :: CardAttribute
+legendary = "legendary"
+lifelink :: CardAttribute
+lifelink = "lifelink"
+planeswalker :: CardAttribute
+planeswalker = "planeswalker"
+sorcery :: CardAttribute
+sorcery = "sorcery"
+storm :: CardAttribute
+storm = "storm"
+summoned :: CardAttribute
+summoned = "summoned"
+undying :: CardAttribute
+undying = "undying"
+tapped :: CardAttribute
+tapped = "tapped"
+token :: CardAttribute
+token = "token"
+trample :: CardAttribute
+trample = "trample"
+triggered :: CardAttribute
+triggered = "triggered"
+vigilance :: CardAttribute
+vigilance = "vigilance"
diff --git a/src/Dovin/Builder.hs b/src/Dovin/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Builder.hs
@@ -0,0 +1,120 @@
+{-|
+Functions for adding new cards to the board.
+
+> withLocation Hand $ do
+>   withAttributes ["angel", token] $ addCreature (4, 4) "Angel"
+-}
+module Dovin.Builder (
+  -- * Builders
+  -- | Each of these terminates a build chain, and will add a card with the
+  -- specified type to the board.
+    addCard
+  , addAura
+  , addArtifact
+  , addCreature
+  , addEnchantment
+  , addInstant
+  , addLand
+  , addLands
+  , addPlaneswalker
+  , addSorcery
+  -- * Fluid interface
+  -- | These methods can be chained together to specify different properties of
+  -- the card to be created.
+  , as
+  , withAttribute
+  , withAttributes
+  , withEffect
+  , withLocation
+  , withPlusOneCounters
+  ) where
+
+import Control.Monad.Reader (ask, local)
+import qualified Data.HashMap.Strict as M
+import qualified Data.Set as S
+
+import Dovin.Attributes
+--import Dovin.Actions
+import Dovin.Prelude
+import Dovin.Types
+
+addCard :: CardName -> GameMonad ()
+addCard name = do
+  card <- use $ cards . at name
+  case card of
+    Just _ -> throwError $ "Card should be removed: " <> name
+    Nothing -> do
+      template <- view envTemplate
+      modifying cards (M.insert name (BaseCard $ set cardName name template))
+
+addAura :: CardName -> GameMonad ()
+addAura name = withAttribute aura $ addEnchantment name
+
+addArtifact :: CardName -> GameMonad ()
+addArtifact name = withAttribute artifact $ addEnchantment name
+
+addCreature :: (Int, Int) -> CardName -> GameMonad ()
+addCreature strength name = local (set (envTemplate . cardStrength) $ mkStrength strength)
+  $ withAttribute creature
+  $ addCard name
+
+addPlaneswalker :: Int -> CardName -> GameMonad ()
+addPlaneswalker loyalty name = local (set (envTemplate . cardLoyalty) loyalty)
+  $ withAttribute planeswalker
+  $ addCard name
+
+addEnchantment :: CardName -> GameMonad ()
+addEnchantment name = withAttribute enchantment $ addCard name
+
+addInstant :: CardName -> GameMonad ()
+addInstant name = withAttribute instant $ addCard name
+
+addLand :: CardName -> GameMonad ()
+addLand name = withAttribute land $ addCard name
+
+addLands :: Int -> CardName -> GameMonad ()
+addLands n name = withAttribute land $
+  forM_ [1..n] $ \n -> addCard (numbered n name)
+
+addSorcery :: CardName -> GameMonad ()
+addSorcery name = withAttribute sorcery $ addCard name
+
+-- | Perform action as the specified player.
+as :: Player -> GameMonad () -> GameMonad ()
+as player = local (set envActor player)
+
+-- | Add an attribute to the created card, as identified by a string.
+-- Attributes with that special meaning to Dovin built-ins (such as flying) are
+-- defined in "Dovin.Attributes".
+withAttribute :: String -> GameMonad () -> GameMonad ()
+withAttribute attr = withAttributes [attr]
+
+-- | Helper version of 'withAttribute' for adding multiple attributes at a
+-- time.
+withAttributes :: [String] -> GameMonad () -> GameMonad ()
+withAttributes attrs =
+  let f = S.union . S.fromList $ attrs in
+  local (over (envTemplate . cardAttributes) f
+       . over (envTemplate . cardDefaultAttributes) f)
+
+-- | Add an effect to the created card.
+withEffect ::
+  CardMatcher -- ^ A matcher that must apply to this card for this affect to
+              -- apply. 'matchInPlay' is a typical value.
+ -> (Card -> CardMatcher) -- ^ Given the current card, return a matcher that
+                          -- matches cards that this affect applies to.
+ -> (Card -> GameMonad Card) -- ^ Apply an effect to the given card.
+ -> GameMonad ()
+ -> GameMonad ()
+withEffect applyCondition filter action =
+  local (over (envTemplate . cardEffects) (mkEffect applyCondition filter action:))
+
+withLocation :: Location -> GameMonad () -> GameMonad ()
+withLocation loc m = do
+  p <- view envActor
+
+  local (set (envTemplate . cardLocation) (p, loc)) m
+
+-- | Set the number of +1/+1 counters of the created card.
+withPlusOneCounters :: Int -> GameMonad () -> GameMonad ()
+withPlusOneCounters = local . set (envTemplate . cardPlusOneCounters)
diff --git a/src/Dovin/Dump.hs b/src/Dovin/Dump.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Dump.hs
@@ -0,0 +1,211 @@
+-- Dumping ground for things that haven't been thought through or tested yet.
+module Dovin.Dump where
+
+import Control.Arrow (second)
+import Control.Lens
+import Control.Monad.Except
+import Control.Monad.State
+import Control.Monad.Writer
+import qualified Data.HashMap.Strict as M
+import qualified Data.Set as S
+import System.Exit
+
+import Dovin.Actions
+import Dovin.Attributes
+import Dovin.Builder
+import Dovin.Formatting
+import Dovin.Helpers
+import Dovin.Monad
+import Dovin.Types
+
+whenMatch :: CardName -> CardMatcher -> GameMonad () -> GameMonad ()
+whenMatch name f action = do
+  match <- requireCard name f >> pure True `catchError` const (pure False)
+
+  when match action
+
+-- ACTIONS
+--
+-- These correspond to things you can do in Magic. They progress the state
+-- machine while verifying applicable properties. They all run inside the
+-- library monad.
+
+target targetName = do
+  card <- requireCard targetName (matchInPlay <> missingAttribute hexproof)
+
+  return ()
+
+targetInLocation zone targetName = do
+  card <- requireCard targetName (matchLocation zone)
+
+  return ()
+
+destroy targetName = do
+  _ <- requireCard targetName (matchInPlay <> missingAttribute indestructible)
+
+  removeFromPlay targetName
+
+sacrifice cn = do
+  actor <- view envActor
+
+  validate (matchController actor) cn
+
+  removeFromPlay cn
+
+removeFromPlay cardName = do
+  card <- requireCard cardName matchInPlay
+
+  moveTo Graveyard cardName
+
+exile cardName = do
+  card <- requireCard cardName mempty
+
+  if hasAttribute "token" card then
+    remove cardName
+  else
+    let loc = view location card in
+      move loc (second (const Exile) loc) cardName
+
+copySpell targetName newName = do
+  card <- requireCard targetName mempty
+
+  let newCard = setAttribute copy . set cardName newName $ card
+
+  modifying
+    cards
+    (M.insert newName $ BaseCard newCard)
+
+  modifying
+    stack
+    ((:) newName)
+
+triggerStorm :: (Int -> GameMonad ()) -> GameMonad ()
+triggerStorm action = do
+  maybeStorm <- use $ counters . at "storm"
+
+  case maybeStorm of
+    Nothing -> throwError "No counter in state: storm"
+    Just c -> forM [1..c-1] $ \n -> action n
+
+  return ()
+
+resetStrength :: CardName -> (Int, Int) -> GameMonad ()
+resetStrength cn desired = do
+  c <- requireCard cn (matchAttribute "creature")
+
+  modifyCard cn cardStrength (const $ mkStrength desired)
+
+modifyStrength :: (Int, Int) -> CardName -> GameMonad ()
+modifyStrength (x, y) cn = do
+  _ <- requireCard cn (matchInPlay <> matchAttribute "creature")
+
+  modifyCard cn cardStrength (CardStrength x y <>)
+
+  -- Fetch card again to get new strength
+  c <- requireCard cn mempty
+
+  when (view cardToughness c <= 0) $ removeFromPlay cn
+
+-- TODO: Better name (resolveMentor?), check source has mentor attribute
+triggerMentor sourceName targetName = do
+  source <- requireCard sourceName $ matchAttribute attacking
+  _      <- requireCard targetName $
+                 matchAttribute attacking
+              <> matchLesserPower (view cardPower source)
+
+  modifyStrength (1, 1) targetName
+
+
+fight :: CardName -> CardName -> GameMonad ()
+fight x y = do
+  cx <- requireCard x (matchInPlay <> matchAttribute creature)
+  cy <- requireCard y (matchInPlay <> matchAttribute creature)
+
+  target x
+  target y
+
+  fight' cx cy
+  unless (cx == cy) $ fight' cy cx
+
+  where
+    fight' cx cy = do
+
+      let xdmg = max 0 $ view cardPower cx
+      modifyCard (view cardName cy) cardDamage (+ xdmg)
+      cy' <- requireCard (view cardName cy) mempty
+
+      when (hasAttribute "lifelink" cx) $
+        do
+          let owner = fst . view location $ cx
+          modifying (life . at owner . non 0) (+ xdmg)
+
+      when (view cardDamage cy' >= view cardToughness cy' || (xdmg > 0 && hasAttribute "deathtouch" cx )) $
+        destroy (view cardName cy)
+
+gainLife :: Player -> Int -> GameMonad ()
+gainLife player amount =
+  modifying
+    (life . at player . non 0)
+    (+ amount)
+
+loseLife :: Player -> Int -> GameMonad ()
+loseLife player amount = gainLife player (-amount)
+
+setLife :: Player -> Int -> GameMonad ()
+setLife p n = assign (life . at p) (Just n)
+
+returnToHand cn = do
+  actor <- view envActor
+  move (actor, Graveyard) (actor, Hand) cn
+
+returnToPlay cn = do
+  actor <- view envActor
+  move (actor, Graveyard) (actor, Play) cn
+
+activatePlaneswalker :: Int -> CardName -> GameMonad ()
+activatePlaneswalker loyalty cn = do
+  c <- requireCard cn matchInPlay
+  actor <- view envActor
+
+  validate (matchController actor) cn
+
+  if view cardLoyalty c - loyalty < 0 then
+    throwError $ cn <> " does not have enough loyalty"
+  else
+    modifyCard cn cardLoyalty (+ loyalty)
+
+
+-- HIGH LEVEL FUNCTIONS
+--
+
+fork :: [GameMonad ()] -> GameMonad ()
+fork options = do
+  b <- get
+
+  forM_ options $ \m -> do
+    m
+    put b
+
+
+with x f = f x
+
+run :: (Int -> Formatter) -> GameMonad () -> IO ()
+run formatter solution = do
+  let (e, _, log) = runMonad emptyBoard solution
+
+  forM_ (zip log [1..]) $ \((step, board), n) -> do
+    putStr $ show n <> ". "
+    putStr step
+    putStrLn (formatter n board)
+
+  putStrLn ""
+  case e of
+    Left x -> do
+      putStrLn "ERROR:"
+      putStrLn x
+      putStrLn ""
+      System.Exit.exitFailure
+    Right _ -> return ()
+
+runVerbose :: GameMonad () -> IO ()
+runVerbose = run (const boardFormatter)
diff --git a/src/Dovin/Formatting.hs b/src/Dovin/Formatting.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Formatting.hs
@@ -0,0 +1,112 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Dovin.Formatting where
+
+import Control.Monad.Writer (Writer, execWriter, tell)
+
+import qualified Data.HashMap.Strict as M
+import qualified Data.Set as S
+import Data.List (intercalate, sort, sortBy, nub)
+import Data.Ord (comparing)
+
+import Dovin.Helpers
+import Dovin.Monad
+import Dovin.Prelude
+import Dovin.Types
+
+type FormatMonad = Writer [(String, GameMonad String)]
+
+blankFormatter :: Formatter
+blankFormatter _ = ""
+
+attributeFormatter :: FormatMonad () -> Formatter
+attributeFormatter m =
+  f $ execWriter m
+  where
+    f :: [(String, GameMonad String)] -> Formatter
+    f attrs board =
+      "\n      " <> (intercalate ", " . map (\(x, y) -> x <> ": " <> y) $
+        map formatAttribute attrs)
+
+      where
+        formatAttribute :: (String, GameMonad String) -> (String, String)
+        formatAttribute (label, m) =
+          let Right value = execMonad board m in
+          (label, value)
+
+stackFormatter :: Formatter
+stackFormatter board =
+  let matchingCs = map lookupCard $ view stack board in
+
+  "\n      Stack:\n" <> formatCards matchingCs
+
+  where
+    lookupCard cn =
+      let Right value = execMonad board (requireCard cn mempty) in value
+
+
+cardFormatter :: String -> CardMatcher -> Formatter
+cardFormatter title matcher board =
+  let matchingCs = sortBy (comparing $ view cardName) . filter (applyMatcher matcher) $ cs in
+
+    "\n      " <> title <> ":\n" <> formatCards matchingCs
+
+  where
+    cs = let Right value = execMonad board allCards in value
+
+formatCards = intercalate "\n" . map (("      " <>) . formatCard)
+
+formatCard c =
+  "  " <> view cardName c <>
+  " (" <> (intercalate "," . sort . S.toList $ view cardAttributes c) <> ")"
+  <> if hasAttribute "creature" c then
+       " ("
+         <> show (view cardPower c)
+         <> "/"
+         <> show (view cardToughness c)
+         <> (let n = view cardPlusOneCounters c in
+               if n > 0 then
+                  ", +" <> show n <> "/+" <> show n
+              else
+                mempty)
+         <> (if view cardDamage c > 0 then
+              ", " <> show (view cardDamage c)
+            else
+              mempty)
+         <> ")"
+     else if hasAttribute "planeswalker" c then
+       " ("
+         <> show (view cardLoyalty c)
+         <> ")"
+     else
+      ""
+
+boardFormatter :: Formatter
+boardFormatter board =
+  let allLocations = nub . sort . map (view location) $ cs in
+
+  let formatters = map
+                     formatLocation
+                     allLocations in
+
+  mconcat formatters board
+
+  where
+    cs = let Right value = execMonad board allCards in value
+    formatLocation (Active, Stack) = stackFormatter
+    formatLocation l = cardFormatter (show l) (matchLocation l)
+
+attribute :: Show a => String -> GameMonad a -> FormatMonad ()
+attribute label m = tell [(label, show <$> m)]
+
+countLife :: Player -> GameMonad Int
+countLife player = use (life . at player . non 0)
+
+countValue :: String -> GameMonad Int
+countValue name = use (counters . at name . non 0)
+
+countCards :: CardMatcher -> GameMonad Int
+countCards matcher =
+  length . filter (applyMatcher matcher) <$> allCards
+
+countManaPool :: Player -> GameMonad Int
+countManaPool p = length <$> use (manaPoolFor p)
diff --git a/src/Dovin/Helpers.hs b/src/Dovin/Helpers.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Helpers.hs
@@ -0,0 +1,182 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Dovin.Helpers where
+
+import Dovin.Types
+import Dovin.Prelude
+
+import Data.List (sort)
+import qualified Data.HashMap.Strict as M
+import qualified Data.Set as S
+import Data.Char (isDigit)
+import Control.Lens (_1, _2, ASetter, both, _Just)
+
+import Text.Parsec
+
+applyMatcherWithDesc :: CardMatcher -> Card -> Either String ()
+applyMatcherWithDesc (CardMatcher d f) c =
+  if f c then
+    Right ()
+  else
+    Left d
+
+hasAttribute attr = S.member attr . view cardAttributes
+
+manaSpec = mconcat <$> many (colorless <|> colored)
+  where
+    colorless = do
+      n <- read <$> many1 digit
+
+      return $ replicate n 'X'
+    colored = many1 (oneOf "RUGBW")
+
+parseMana :: String -> ManaPool
+-- sort puts the Xs at the back
+parseMana pool =
+  case parse manaSpec "mana" pool of
+    Left err -> mempty
+    Right x -> sort x
+
+requireCard :: CardName -> CardMatcher -> GameMonad Card
+requireCard name f = do
+  maybeCard <- use $ cards . at name
+
+  case maybeCard of
+    Nothing -> throwError $ "Card does not exist: " <> name
+    Just card -> do
+      card' <- applyEffects card
+      case applyMatcherWithDesc f card' of
+        Right () -> return card'
+        Left msg ->
+          throwError $ name <> " does not match requirements: " <> msg
+
+applyEffects :: BaseCard -> GameMonad Card
+applyEffects (BaseCard card) = do
+  cs <- map unwrap . M.elems <$> use cards
+
+  let allEffects =
+        concatMap
+          (\c -> map (\e -> (e, c)) . view cardEffects $ c)
+          cs
+
+  let enabledEffects =
+        filter
+          (\(e, c) -> applyMatcher (view effectEnabled e) c)
+          allEffects
+
+  let applicableEffects =
+        filter
+          (\(e, c) -> applyMatcher (view effectFilter e c) card)
+          enabledEffects
+
+  card' <- foldM (\c (e, _) -> applyEffect2 c e) card applicableEffects
+
+  let counterModifier = mconcat
+                          . replicate (view cardPlusOneCounters card')
+                          . mkStrength $ (1, 1)
+
+  return $ over cardStrength (counterModifier <>) card'
+
+  where
+    applyEffect2 :: Card -> CardEffect -> GameMonad Card
+    applyEffect2 card e = view effectAction e card
+
+    unwrap :: BaseCard -> Card
+    unwrap (BaseCard card) = card
+
+allCards :: GameMonad [Card]
+allCards = do
+  bases <- M.elems <$> use cards
+
+  mapM applyEffects bases
+
+modifyCard :: CardName -> ASetter Card Card a b -> (a -> b) -> GameMonad ()
+modifyCard name lens f =
+  modifying
+    (cards . at name . _Just)
+    (\(BaseCard c) -> BaseCard $ over lens f c)
+
+-- CARD MATCHERS
+--
+-- Matchers are used for both filtering sets of cards, and also for verifying
+-- attributes of cards.
+--
+-- A wrapping type is used since I intend to add labels/introspection
+-- capabilities at some point.
+matchDamage :: Int -> CardMatcher
+matchDamage n = CardMatcher (show n <> " damage") $
+  (==) n . view cardDamage
+
+matchLoyalty :: Int -> CardMatcher
+matchLoyalty n = CardMatcher (show n <> " loyalty") $
+  (==) n . view cardLoyalty
+
+matchPlusOneCounters :: Int -> CardMatcher
+matchPlusOneCounters n = CardMatcher (show n <> " +1/+1 counters") $
+  (==) n . view cardPlusOneCounters
+
+matchLocation :: CardLocation -> CardMatcher
+matchLocation loc = CardMatcher ("in location " <> show loc) $
+  (==) loc . view cardLocation
+
+matchInPlay = CardMatcher "in play" $ \c -> snd (view location c) == Play
+
+matchAttribute :: CardAttribute -> CardMatcher
+matchAttribute attr = CardMatcher ("has attribute " <> attr) $
+  S.member attr . view cardAttributes
+
+matchAttributes :: [CardAttribute] -> CardMatcher
+matchAttributes = foldr ((<>) . matchAttribute) mempty
+
+matchName :: CardName -> CardMatcher
+matchName n = CardMatcher ("has name " <> n) $ (==) n . view cardName
+
+matchOtherCreatures :: Card -> CardMatcher
+matchOtherCreatures card = matchLocation (view cardLocation card) <> invert (matchName (view cardName card))
+
+matchController player = CardMatcher ("has controller " <> show player) $
+  (==) player . view (location . _1)
+
+matchLesserPower n = CardMatcher ("power < " <> show n) $
+  (< n) . view cardPower
+
+missingAttribute = invert . matchAttribute
+
+(CardMatcher d1 f) `matchOr` (CardMatcher d2 g) =
+    CardMatcher (d1 <> " or " <> d2) $ \c -> f c || g c
+
+invert :: CardMatcher -> CardMatcher
+invert (CardMatcher d f) = CardMatcher ("not " <> d) $ not . f
+
+labelMatch :: String -> CardMatcher -> CardMatcher
+labelMatch label (CardMatcher d f) = CardMatcher label f
+applyMatcher :: CardMatcher -> Card -> Bool
+applyMatcher matcher c =
+  case applyMatcherWithDesc matcher c of
+    Left _ -> False
+    Right _ -> True
+
+loseAttribute attr cn = do
+  c <- requireCard cn mempty
+
+  modifyCard cn id (removeAttribute attr)
+
+removeAttribute :: CardAttribute -> Card -> Card
+removeAttribute attr = over cardAttributes (S.delete attr)
+
+gainAttribute attr cn = do
+  c <- requireCard cn mempty
+
+  modifyCard cn id (setAttribute attr)
+
+setAttribute :: CardAttribute -> Card -> Card
+setAttribute attr = over cardAttributes (S.insert attr)
+
+forCards :: CardMatcher -> (CardName -> GameMonad ()) -> GameMonad ()
+forCards matcher f = do
+  cs <- allCards
+
+  let matchingCs = filter (applyMatcher matcher) cs
+
+  forM_ (map (view cardName) matchingCs) f
+
diff --git a/src/Dovin/Monad.hs b/src/Dovin/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Monad.hs
@@ -0,0 +1,22 @@
+module Dovin.Monad where
+
+import           Control.Monad.Identity
+import           Control.Monad.Except
+import           Control.Monad.Writer
+import           Control.Monad.Reader
+import           Control.Monad.State hiding (state)
+
+import Dovin.Types
+
+runMonad :: Board -> GameMonad () -> (Either String (), Board, [(String, Board)])
+runMonad state m =
+  let ((e, b), log) = runIdentity $
+                        runWriterT (runStateT (runReaderT (runExceptT m) emptyEnv) state) in
+
+  (e, b, log)
+
+execMonad :: Board -> GameMonad a -> Either String a
+execMonad state m =
+  let result = fst $ runIdentity (runWriterT (evalStateT (runReaderT (runExceptT m) emptyEnv) state)) in
+
+  result
diff --git a/src/Dovin/Prelude.hs b/src/Dovin/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Prelude.hs
@@ -0,0 +1,11 @@
+-- | Re-exports common internal imports. Not recommended for external use.
+module Dovin.Prelude
+  ( module Control.Lens
+  , module Control.Monad
+  , module Control.Monad.Except
+  )
+  where
+
+import Control.Lens (assign, at, modifying, non, over, set, use, view)
+import Control.Monad (foldM, forM_, unless, when)
+import Control.Monad.Except (catchError, throwError)
diff --git a/src/Dovin/Types.hs b/src/Dovin/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/Types.hs
@@ -0,0 +1,210 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+module Dovin.Types where
+
+import Control.Lens (Lens', Prism', makeLenses, over, view, _1, _Just, at, non)
+import Control.Monad.Reader (ReaderT)
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Identity (Identity)
+import Control.Monad.State (StateT)
+import Control.Monad.Writer (WriterT)
+import qualified Data.HashMap.Strict as M
+import Data.Hashable (Hashable)
+import qualified Data.Set as S
+import GHC.Generics
+
+type CardName = String
+type CardAttribute = String
+data Player = Active | Opponent deriving (Show, Eq, Generic, Ord)
+-- This is pretty dodgy - one char per mana - but works for now.
+type ManaPool = String
+type ManaString = String
+-- TODO: Stack shouldn't be in here because there is only one of them
+data Location = Hand | Graveyard | Play | Stack | Exile
+  deriving (Show, Eq, Ord)
+
+data CardEffect = CardEffect
+  { _effectEnabled :: CardMatcher
+  , _effectFilter :: Card -> CardMatcher
+  , _effectAction :: Card -> GameMonad Card
+  }
+
+mkEffect enabled filter action = CardEffect
+  -- For an effect to be enabled, it's host card must currently match this
+  -- matcher.
+  { _effectEnabled = enabled
+  -- If the effect is enabled, this filter determines wheter any particular
+  -- card is affected by it.
+  , _effectFilter = filter
+  -- The action to apply to affected cards.
+  , _effectAction = action
+  }
+
+-- A target for a spell or ability.
+data Target =
+    TargetPlayer Player -- ^ Target a player, use 'targetPlayer' to construct.
+  | TargetCard CardName -- ^ Target a card, use 'targetCard' to construct.
+
+targetPlayer = TargetPlayer
+targetCard = TargetCard
+
+type CardLocation = (Player, Location)
+type CardAttributes = S.Set CardAttribute
+data CardStrength = CardStrength Int Int deriving (Eq)
+instance Show CardStrength where
+  show (CardStrength p t) = show p <> "/" <> show t
+
+-- | A phase or step in a turn. Phases and steps are not distinguished between
+-- because haven't seen a need to.
+data Phase
+  = Untap
+  | Upkeep
+  | DrawStep
+  | FirstMain
+  | BeginCombat
+  | DeclareAttackers
+  | DeclareBlockers
+  | FirstStrikeDamage
+  | CombatDamage
+  | EndCombat
+  | SecondMain
+  | EndStep
+  deriving (Show, Eq, Ord)
+
+data Card = Card
+  { _cardName :: CardName
+  , _location :: (Player, Location)
+  , _cardDefaultAttributes :: CardAttributes
+  , _cardAttributes :: CardAttributes
+  , _cardStrength :: CardStrength
+  , _cardDamage :: Int
+  , _cardLoyalty :: Int
+  , _cardEffects :: [CardEffect]
+
+  -- Can probably generalize this more at some point.
+  , _cardPlusOneCounters :: Int
+  }
+instance Hashable Player
+instance Show Card where
+  show = _cardName
+instance Eq Card where
+  a == b = _cardName a == _cardName b
+
+newtype BaseCard = BaseCard Card deriving (Show, Eq)
+
+data CardMatcher = CardMatcher String (Card -> Bool)
+type EffectName = String
+
+data Board = Board
+  { _cards :: M.HashMap CardName BaseCard
+  -- The stack is currently the only location where we care about order, so
+  -- store that information alongside the main _cards map. This won't scale -
+  -- deck and graveyard need to be ordered also - but works for now. Need to
+  -- think more about "hiding" this data structure.
+  , _stack :: [CardName]
+  , _counters :: M.HashMap String Int
+  -- In theory, life could be just another counter. Need to think more about
+  -- making that happen.
+  , _life :: M.HashMap Player Int
+  , _manaPool :: M.HashMap Player ManaPool
+  , _phase :: Phase
+  }
+
+data Env = Env
+  { _envTemplate :: Card
+  , _envSBAEnabled :: Bool
+  , _envActor :: Player
+  }
+
+type GameMonad a = (ExceptT String (ReaderT Env (StateT Board (WriterT [(String, Board)] Identity)))) a
+type Formatter = Board -> String
+
+makeLenses ''Board
+makeLenses ''Card
+makeLenses ''CardEffect
+makeLenses ''Env
+
+cardLocation :: Control.Lens.Lens' Card (Player, Location)
+cardLocation = location
+
+cardOwner :: Control.Lens.Lens' Card Player
+cardOwner = cardLocation . _1
+
+-- TODO: How to define these lenses using built-in Lens primitives
+-- (Control.Lens.Wrapped?)
+cardPower :: Control.Lens.Lens' Card Int
+cardPower f parent = fmap
+  (\x -> over cardStrength (setPower x) parent)
+  (f . power . view cardStrength $ parent)
+  where
+    setPower p (CardStrength _ t) = CardStrength p t
+    power (CardStrength p _) = p
+
+cardToughness :: Control.Lens.Lens' Card Int
+cardToughness f parent = fmap
+  (\x -> over cardStrength (setToughness x) parent)
+  (f . toughness . view cardStrength $ parent)
+  where
+    setToughness t (CardStrength p _) = CardStrength p t
+    toughness (CardStrength _ t) = t
+
+
+manaPoolFor p = manaPool . at p . non mempty
+
+-- I can't figure out the right type signature for manaPoolFor, so instead
+-- providing this function to make it inferrable.
+_manaPoolForTyping :: Board -> ManaPool
+_manaPoolForTyping = view (manaPoolFor Active)
+
+instance Show CardMatcher where
+  show _ = "<matcher>"
+
+instance Semigroup CardMatcher where
+  (CardMatcher d1 f) <> (CardMatcher d2 g) =
+    CardMatcher (d1 <> " and " <> d2) $ \c -> f c && g c
+
+instance Monoid CardMatcher where
+  mempty = CardMatcher "" $ const True
+
+instance Semigroup CardStrength where
+  CardStrength p1 t1 <> CardStrength p2 t2 =
+   CardStrength (p1 + p2) (t1 + t2)
+
+instance Monoid CardStrength where
+  mempty = CardStrength 0 0
+
+emptyEnv = Env
+  { _envTemplate = emptyCard
+  , _envSBAEnabled = True
+  , _envActor = Active
+  }
+
+mkStrength (p, t) = CardStrength p t
+emptyCard = mkCard "" (Active, Hand)
+mkCard name location =
+  Card
+    { _cardName = name
+    , _location = location
+    , _cardDefaultAttributes = mempty
+    , _cardAttributes = mempty
+    , _cardStrength = mempty
+    , _cardDamage = 0
+    , _cardLoyalty = 0
+    , _cardEffects = mempty
+    , _cardPlusOneCounters = 0
+    }
+
+opposing :: Player -> Player
+opposing Active = Opponent
+opposing Opponent = Active
+
+emptyBoard = Board
+               { _cards = mempty
+               , _counters = mempty
+               , _stack = mempty
+               , _life = mempty
+               , _manaPool = mempty
+               , _phase = FirstMain
+               }
+
diff --git a/src/Dovin/V1.hs b/src/Dovin/V1.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/V1.hs
@@ -0,0 +1,69 @@
+module Dovin.V1
+  ( module Dovin.Dump
+  , module Dovin.Actions
+  , module Dovin.Attributes
+  , module Dovin.Builder
+  , module Dovin.Formatting
+  , module Dovin.Helpers
+  , module Dovin.Types
+  , validate
+  , validateLife
+  , withLocation
+  , activate
+  , trigger
+  ) where
+
+import Dovin.Dump
+import Dovin.Actions hiding (validate, validateLife, activate, trigger)
+import qualified Dovin.Actions
+import Dovin.Attributes
+import Dovin.Builder hiding (withLocation)
+import Dovin.Formatting
+import Dovin.Helpers
+import Dovin.Monad
+import Dovin.Types
+
+import Control.Monad.Reader (local)
+import Control.Lens (set, view)
+
+-- | Validate that a card matches a matcher.
+--
+-- > validate "Angrath's Marauders" $ matchAttribute "pirate"
+--
+-- [Validates]
+--
+--   * Card matches matcher.
+validate :: CardName -> CardMatcher -> GameMonad ()
+validate = flip Dovin.Actions.validate
+
+-- | Validates a player has a specific life total.
+--
+-- > validateLife Opponent 0
+--
+-- [Validates]
+--
+--     * Player life equals amount.
+validateLife :: Player -> Int -> GameMonad ()
+validateLife = flip Dovin.Actions.validateLife
+
+-- | Set the location of the created card.
+withLocation :: CardLocation -> GameMonad () -> GameMonad ()
+withLocation loc = local (set (envTemplate . cardLocation) loc)
+
+activate mana targetName = do
+  card <- requireCard targetName mempty
+  actor <- view envActor
+
+  validate targetName $ matchController actor
+
+  spendMana mana
+
+  return ()
+
+trigger targetName = do
+  -- TODO: Technically some cards can trigger from other zones, figure out best
+  -- way to represent.
+  card <- requireCard targetName matchInPlay
+
+  return ()
+
diff --git a/src/Dovin/V2.hs b/src/Dovin/V2.hs
new file mode 100644
--- /dev/null
+++ b/src/Dovin/V2.hs
@@ -0,0 +1,29 @@
+-- V2 makes the following changes from V1:
+--
+--   * withLocation now only takes a Location, using the current actor for
+--     player.
+--   * Flips argument order for `validate` functions to be consistent with rest
+--     of API.
+--   * `activate` and `trigger` use the stack.
+module Dovin.V2
+  ( module Dovin.Dump
+  , module Dovin.Actions
+  , module Dovin.Attributes
+  , module Dovin.Builder
+  , module Dovin.Formatting
+  , module Dovin.Helpers
+  , module Dovin.Types
+  )
+  where
+
+import Dovin.Actions
+import qualified Dovin.V1
+import Dovin.Prelude
+import Dovin.Dump hiding (activate, trigger)
+import Dovin.Attributes
+import Dovin.Builder
+import Dovin.Formatting
+import Dovin.Helpers
+import Dovin.Monad
+import Dovin.Types
+import Control.Monad.Reader (local)
diff --git a/src/Lib.hs b/src/Lib.hs
new file mode 100644
--- /dev/null
+++ b/src/Lib.hs
@@ -0,0 +1,6 @@
+module Lib
+    ( someFunc
+    ) where
+
+someFunc :: IO ()
+someFunc = putStrLn "someFunc"
diff --git a/src/Solutions.hs b/src/Solutions.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions.hs
@@ -0,0 +1,28 @@
+module Solutions where
+import qualified Solutions.Channel
+import qualified Solutions.Core19_9
+import qualified Solutions.Dominaria5
+import qualified Solutions.Example
+import qualified Solutions.ExplorersOfIxalanContest
+import qualified Solutions.GuildsOfRavnica1
+import qualified Solutions.GuildsOfRavnica3
+import qualified Solutions.GuildsOfRavnica8
+import qualified Solutions.GuildsOfRavnica9
+import qualified Solutions.GuildsOfRavnicaPre2
+import qualified Solutions.RivalsOfIxalan7
+import qualified Solutions.UltimateMasters
+
+all = [
+  ("Channel", Solutions.Channel.solution, Solutions.Channel.formatter),
+  ("Core19_9", Solutions.Core19_9.solution, Solutions.Core19_9.formatter),
+  ("Dominaria5", Solutions.Dominaria5.solution, Solutions.Dominaria5.formatter),
+  ("Example", Solutions.Example.solution, Solutions.Example.formatter),
+  ("ExplorersOfIxalanContest", Solutions.ExplorersOfIxalanContest.solution, Solutions.ExplorersOfIxalanContest.formatter),
+  ("GuildsOfRavnica1", Solutions.GuildsOfRavnica1.solution, Solutions.GuildsOfRavnica1.formatter),
+  ("GuildsOfRavnica3", Solutions.GuildsOfRavnica3.solution, Solutions.GuildsOfRavnica3.formatter),
+  ("GuildsOfRavnica8", Solutions.GuildsOfRavnica8.solution, Solutions.GuildsOfRavnica8.formatter),
+  ("GuildsOfRavnica9", Solutions.GuildsOfRavnica9.solution, Solutions.GuildsOfRavnica9.formatter),
+  ("GuildsOfRavnicaPre2", Solutions.GuildsOfRavnicaPre2.solution, Solutions.GuildsOfRavnicaPre2.formatter),
+  ("RivalsOfIxalan7", Solutions.RivalsOfIxalan7.solution, Solutions.RivalsOfIxalan7.formatter),
+  ("UltimateMasters", Solutions.UltimateMasters.solution, Solutions.UltimateMasters.formatter)
+  ]
diff --git a/src/Solutions/Channel.hs b/src/Solutions/Channel.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/Channel.hs
@@ -0,0 +1,355 @@
+module Solutions.Channel where
+
+import Dovin.V2
+import Dovin.Prelude
+
+import Data.List (delete)
+import Control.Lens
+import Debug.Trace
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Active 1
+
+    withLocation Play $ do
+      addLands 4 "Steam Vents"
+      addLands 4 "Breeding Pool"
+      addArtifact "Aetherflux Reservoir"
+      addCreature (2, 2) "Beamsplitter Mage"
+      addCreature (2, 2) "Man-o'-War"
+
+    withLocation Hand $ do
+      addInstant "High Tide"
+      addInstant "Snap"
+      addInstant "Rewind"
+      addSorcery "Baral's Expertise"
+      addSorcery "Channel"
+      addSorcery "Fireball"
+      withAttribute flash $ addCreature (2, 1) "Snapcaster Mage"
+      addCreature (0, 0) "Walking Ballista"
+
+  step "Cast High Tide with a Steam Vents" $ do
+    tapForManaWithTide "U" "Steam Vents 1"
+    withTriggers (cast "U") "High Tide"
+    resolveAetherflux 1
+    resolve "High Tide"
+
+    modifying
+      highTideCounter
+      (+ 1)
+
+  step "Cast Snapcaster, targeting High Tide, with second Steam Vents" $ do
+    tapForManaWithTide "U" "Steam Vents 2"
+    withTriggers (cast "1U") "Snapcaster Mage"
+
+    resolveAetherflux 2
+    resolve "Snapcaster Mage"
+    targetInLocation (Active, Graveyard) "High Tide"
+    gainAttribute snapped "High Tide"
+
+  step "Flashback High Tide with third Steam Vents" $ do
+    tapForManaWithTide "U" "Steam Vents 3"
+    withTriggers (flashbackSnapped "U") "High Tide"
+
+    resolveAetherflux 3
+    resolve "High Tide"
+
+    modifying
+      highTideCounter
+      (+ 1)
+
+  step "Tap five remaining lands for 3 mana each" $ do
+    tapForManaWithTide "R" "Steam Vents 4"
+    tapForManaWithTide "G" "Breeding Pool 1"
+    tapForManaWithTide "G" "Breeding Pool 2"
+    tapForManaWithTide "U" "Breeding Pool 3"
+    tapForManaWithTide "U" "Breeding Pool 4"
+
+  step "Cast Walking Ballista for 1, leave on stack" $ do
+    withTriggers (cast "") "Walking Ballista"
+
+  step "Stack Snap, targeting Beamsplitter then copying to Snapcaster" $ do
+    withTriggers (cast "1U") "Snap"
+    target "Beamsplitter Mage"
+    trigger "Copied Snap" "Beamsplitter Mage" >> resolveTop
+    copySpell "Snap" "Snap Copy (Snapcaster Mage)"
+    target "Snapcaster Mage"
+
+  step "Counter Walking Ballista with Rewind, untapping Steam Vents" $ do
+    withTriggers (cast "2UU") "Rewind"
+    counter "Walking Ballista"
+    resolveAetherflux 6
+    resolve "Rewind"
+    untap "Steam Vents 1"
+    untap "Steam Vents 2"
+    untap "Steam Vents 3"
+    untap "Steam Vents 4"
+
+  step "Resolve Snap copy, returning Snapcaster, untapping Breeding Pools" $ do
+    resolve "Snap Copy (Snapcaster Mage)"
+
+    move (Active, Play) (Active, Hand) "Snapcaster Mage"
+    untap "Breeding Pool 1"
+    untap "Breeding Pool 2"
+
+  step "Resolve Snap, returning Beamsplitter, untapping Breeding Pools" $ do
+    resolveAetherflux 5
+    resolve "Snap"
+    move (Active, Play) (Active, Hand) "Beamsplitter Mage"
+    untap "Breeding Pool 3"
+    untap "Breeding Pool 4"
+    resolveAetherflux 4
+
+  step "Recast Beamsplitter, stacking Snapcaster targeting Snap" $ do
+    withTriggers (cast "RU") "Beamsplitter Mage"
+    withTriggers (cast "1U") "Snapcaster Mage"
+
+    resolveAetherflux 8
+    resolve "Snapcaster Mage"
+    resolveAetherflux 7
+    resolve "Beamsplitter Mage"
+
+    targetInLocation (Active, Graveyard) "Snap"
+    gainAttribute snapped "Snap"
+
+  step "Tap all lands for 3 mana each" $ do
+    tapForManaWithTide "U" "Steam Vents 1"
+    tapForManaWithTide "U" "Steam Vents 2"
+    tapForManaWithTide "R" "Steam Vents 3"
+    tapForManaWithTide "R" "Steam Vents 4"
+    tapForManaWithTide "G" "Breeding Pool 1"
+    tapForManaWithTide "G" "Breeding Pool 2"
+    tapForManaWithTide "U" "Breeding Pool 3"
+    tapForManaWithTide "U" "Breeding Pool 4"
+
+  step "Stack flashbacked Snap, targeting Beamsplitter then copy to Snapcaster" $ do
+    withTriggers (flashbackSnapped "1U") "Snap"
+    target "Beamsplitter Mage"
+    trigger "Copied Snap" "Beamsplitter Mage" >> resolveTop
+    copySpell "Snap" "Snap Copy (Snapcaster Mage)"
+    target "Snapcaster Mage"
+
+  step "Resolve Snap copy, returning Snapcaster, untap Breeding Pools" $ do
+    resolve "Snap Copy (Snapcaster Mage)"
+
+    move (Active, Play) (Active, Hand) "Snapcaster Mage"
+    untap "Breeding Pool 1"
+    untap "Breeding Pool 2"
+
+  step "Replay Snapcaster, targeting Rewind" $ do
+    withTriggers (cast "1U") "Snapcaster Mage"
+    resolveAetherflux 10
+    resolve "Snapcaster Mage"
+    targetInLocation (Active, Graveyard) "Rewind"
+    gainAttribute snapped "Rewind"
+
+  step "Resolve Snap on Beamsplitter, untap Steam Vents" $ do
+    resolveAetherflux 9
+    resolve "Snap"
+    move (Active, Play) (Active, Hand) "Beamsplitter Mage"
+    untap "Steam Vents 3"
+    untap "Steam Vents 4"
+
+  step "Cast Baral's Expertise for all 3 in play, replaying Aetherflux for free" $ do
+    withTriggers (cast "3UU") "Baral's Expertise"
+    resolveAetherflux 11
+    resolve "Baral's Expertise"
+
+    move (Active, Play) (Active, Hand) "Aetherflux Reservoir"
+    move (Active, Play) (Active, Hand) "Man-o'-War"
+    move (Active, Play) (Active, Hand) "Snapcaster Mage"
+
+    withTriggers (cast "") "Aetherflux Reservoir"
+    resolve "Aetherflux Reservoir"
+
+  step "Cast Beamsplitter Mage, stacking Snapcaster targeting Baral's" $ do
+    withTriggers (cast "UR") "Beamsplitter Mage"
+    withTriggers (cast "1U") "Snapcaster Mage"
+    resolveAetherflux 14
+    resolve "Snapcaster Mage"
+    resolveAetherflux 13
+    resolve "Beamsplitter Mage"
+
+    targetInLocation (Active, Graveyard) "Baral's Expertise"
+    gainAttribute snapped "Baral's Expertise"
+
+  step "Flashback Baral's Expertise targeting all 3 in play, replaying Aetherflux" $ do
+    withTriggers (flashbackSnapped "3UU") "Baral's Expertise"
+    resolveAetherflux 15
+    resolve "Baral's Expertise"
+
+    move (Active, Play) (Active, Hand) "Aetherflux Reservoir"
+    move (Active, Play) (Active, Hand) "Beamsplitter Mage"
+    move (Active, Play) (Active, Hand) "Snapcaster Mage"
+
+    withTriggers (cast "") "Aetherflux Reservoir"
+    resolve "Aetherflux Reservoir"
+
+  step "Tap remaining lands for 3 mana each" $ do
+    tapForManaWithTide "G" "Breeding Pool 1"
+    tapForManaWithTide "G" "Breeding Pool 2"
+    tapForManaWithTide "R" "Steam Vents 3"
+    tapForManaWithTide "R" "Steam Vents 4"
+
+  step "Cast Channel and Fireball for life only" $ do
+    withTriggers (cast "GG") "Channel"
+    resolveAetherflux 17
+    resolve "Channel"
+
+    l <- (-) <$> countLife Active <*> pure 1
+
+    let payment = show l <> "R"
+
+    loseLife Active l
+    addMana $ show l
+
+    withTriggers (cast payment) "Fireball"
+    resolveAetherflux 18
+    resolve "Fireball"
+
+    damage (const l) (targetPlayer Opponent) "Fireball"
+
+  step "Cast Beamsplitter Mage, stacking Snapcaster targeting Fireball" $ do
+    withTriggers (cast "UR") "Beamsplitter Mage"
+    withTriggers (cast "1U") "Snapcaster Mage"
+    resolveAetherflux 20
+    resolve "Snapcaster Mage"
+    resolveAetherflux 19
+    resolve "Beamsplitter Mage"
+
+    targetInLocation (Active, Graveyard) "Fireball"
+    gainAttribute snapped "Fireball"
+
+  step "Cast Man-'o-War, returning Snapcaster Mage" $ do
+    withTriggers (cast "2U") "Man-o'-War"
+    resolveAetherflux 21
+    resolve "Man-o'-War"
+
+    target "Snapcaster Mage"
+    move (Active, Play) (Active, Hand) "Snapcaster Mage"
+
+  step "Cast Snapcaster, counter with flashback Rewind" $ do
+    withTriggers (cast "1U") "Snapcaster Mage"
+    withTriggers (flashbackSnapped "2UU") "Rewind"
+    resolveAetherflux 23
+    resolve "Rewind"
+    counter "Snapcaster Mage"
+    resolveAetherflux 22
+
+    untap "Breeding Pool 1"
+    untap "Breeding Pool 2"
+    untap "Steam Vents 3"
+    untap "Steam Vents 4"
+
+  step "Flashback Fireball with all remaining mana and life" $ do
+    tapForManaWithTide "U" "Breeding Pool 1"
+    tapForManaWithTide "U" "Breeding Pool 2"
+    tapForManaWithTide "R" "Steam Vents 3"
+    tapForManaWithTide "R" "Steam Vents 4"
+
+    life <- countLife Active
+    mana <- countManaPool Active
+    let dmg = (life - 1) + (mana - 1)
+    let payment = show dmg <> "R"
+
+    loseLife Active (life - 1)
+    addMana $ show (life - 1)
+
+    withTriggers (flashbackSnapped payment) "Fireball"
+    resolveAetherflux 24
+    resolve "Fireball"
+
+    damage (const life) (targetPlayer Opponent) "Fireball"
+
+attributes = attributeFormatter $ do
+  attribute "life" $ countLife Active
+  attribute "pool" $ countManaPool Active
+  attribute "spells" $ use spellCounter
+
+playExLandFormatter = cardFormatter "Play (ex. Land)"
+  (matchLocation (Active, Play) <> invert (matchAttribute land))
+formatter 1 = attributes <> boardFormatter
+formatter 3 = attributes
+  <> cardFormatter "Play" (matchLocation (Active, Play))
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 6 = attributes <> stackFormatter
+formatter 7 = attributes <> stackFormatter
+formatter 8 = attributes <> stackFormatter
+  <> cardFormatter "Play" (matchLocation (Active, Play))
+formatter 9 = attributes <> stackFormatter
+formatter 10 = attributes <> stackFormatter
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 11 = attributes
+  <> cardFormatter "Play" (matchLocation (Active, Play))
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 13 = attributes <> stackFormatter
+formatter 14 = attributes <> stackFormatter
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 15 = attributes <> stackFormatter
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 16 = attributes
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> cardFormatter "Play" (matchLocation (Active, Play))
+formatter 17 = attributes
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> playExLandFormatter
+formatter 18 = attributes
+  <> playExLandFormatter
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 19 = attributes
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> playExLandFormatter
+formatter 21 = attributeFormatter (attribute "opponent" $ countLife Opponent) <> attributes
+formatter 22 = attributes
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> playExLandFormatter
+  <> cardFormatter "Graveyard" (matchLocation (Active, Graveyard))
+formatter 23 = attributes
+  <> cardFormatter "Hand" (matchLocation (Active, Hand))
+  <> playExLandFormatter
+formatter 25 = attributeFormatter (attribute "opponent" $ countLife Opponent) <> attributes
+formatter _ = attributes
+
+spellCounter :: Lens' Board Int
+spellCounter = counters . at "spell-count" . non 0
+
+highTideCounter :: Lens' Board Int
+highTideCounter = counters . at "high-tide-count" . non 0
+
+aetherfluxTriggerName n = "Aetherflux Trigger #" <> show n
+snapped = "snapped"
+
+-- Keeps track of number of spells cast, and if Aetherflux Reservoir is in play
+-- triggers it.
+withTriggers fn name = do
+  fn name
+
+  modifying
+    spellCounter
+    (+ 1)
+
+  forCards
+    (matchInPlay <> matchName "Aetherflux Reservoir")
+    $ const $ do
+      x <- use spellCounter
+      trigger (aetherfluxTriggerName x) "Aetherflux Reservoir"
+
+tapForManaWithTide pool cn = do
+  tapForMana pool cn
+  x <- use highTideCounter
+
+  addMana (replicate x 'U')
+
+resolveAetherflux n = do
+  resolve $ aetherfluxTriggerName n
+
+  x <- use spellCounter
+  gainLife Active x
+
+flashbackSnapped mana castName = do
+  validate (matchAttribute snapped) castName
+  flashback mana castName
+
diff --git a/src/Solutions/Core19_9.hs b/src/Solutions/Core19_9.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/Core19_9.hs
@@ -0,0 +1,150 @@
+module Solutions.Core19_9 where
+
+import Dovin.V1
+import Dovin.Prelude
+
+spellCount = "spell-count"
+
+-- Keeps track of number of spells cast, and if Aetherflux Reservoir is in play
+-- triggers it.
+castWithTriggers cost name = do
+  modifying
+    (counters . at spellCount . non 0)
+    (+ 1)
+
+  forCards
+    (matchInPlay <> matchName "Aetherflux Reservoir")
+    $ const $ do
+      trigger "Aetherflux Reservoir"
+      x <- use $ counters . at spellCount . non 0
+      gainLife Active x
+
+  cast cost name
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 50
+    setLife Active 1
+
+    withLocation (Active, Play) $ do
+      addLands 3 "Spirebluff Canal"
+      addArtifact "Cultivator's Caravan"
+      addArtifact "Powerstone Shard 1"
+      addArtifact "Powerstone Shard 2"
+      addArtifact "Mox Amber 1"
+      addCreature (2, 2) "Captain Lannery Storm"
+
+    withLocation (Active, Hand) $ do
+      addArtifact "Aetherflux Reservoir"
+      addArtifact "Mox Amber 2"
+      addInstant "Paradoxical Outcome"
+      addArtifact "Foundry Inspector"
+      addInstant "Abrade"
+
+  step "Attack with Captain to get a Treasure, assume he's blocked and destroyed" $ do
+    attackWith ["Captain Lannery Storm"]
+    withLocation (Active, Play) $ withAttribute token $ addArtifact "Treasure"
+
+    destroy "Captain Lannery Storm"
+    transitionTo SecondMain
+
+  step "Cast Foundry Inspector, reducing cost of future artifacts" $ do
+    tapForMana "1" "Treasure"
+    sacrifice "Treasure"
+    tapForMana "U" "Spirebluff Canal 1"
+    tapForMana "U" "Spirebluff Canal 2"
+    castWithTriggers "3" "Foundry Inspector" >> resolveTop
+
+  step "Cast Aetherflux Reservoir" $ do
+    tapForMana "2" "Powerstone Shard 1"
+    tapForMana "U" "Spirebluff Canal 3"
+    castWithTriggers "3" "Aetherflux Reservoir" >> resolveTop
+
+  step "Cast Mox Amber" $ do
+    castWithTriggers "" "Mox Amber 2" >> resolveTop
+
+  step "Tap Cultivator's Caravan, leave mana floating" $ do
+    tapForMana "U" "Cultivator's Caravan"
+
+  step "Cast Paradoxical Outcome for all artifacts and a tapped land" $ do
+    tapForMana "2" "Powerstone Shard 2"
+    tapForMana "U" "Mox Amber 1"
+    tapForMana "U" "Mox Amber 2"
+    castWithTriggers "3U" "Paradoxical Outcome" >> resolveTop
+
+    moveTo Hand "Spirebluff Canal 1"
+    moveTo Hand "Powerstone Shard 1"
+    moveTo Hand "Powerstone Shard 2"
+    moveTo Hand "Mox Amber 1"
+    moveTo Hand "Mox Amber 2"
+    moveTo Hand "Cultivator's Caravan"
+
+  step "Replay land and moxes" $ do
+    moveTo Play "Spirebluff Canal 1"
+    forM_ [1..2] $ \n -> do
+      castWithTriggers "" (numbered n "Mox Amber") >> resolveTop
+
+  step "Replay Powerstone Shard 1 with moxes" $ do
+    tapForMana "1" "Mox Amber 1"
+    tapForMana "1" "Mox Amber 2"
+    castWithTriggers "2" "Powerstone Shard 1" >> resolveTop
+
+  step "Replay Powerstone Shard 2 with floating mana and land" $ do
+    tapForMana "U" "Spirebluff Canal 1"
+    castWithTriggers "2" "Powerstone Shard 2" >> resolveTop
+
+  step "Replay Caravan" $ do
+    tapForMana "2" "Powerstone Shard 1"
+    castWithTriggers "2" "Cultivator's Caravan" >> resolveTop
+
+  step "Cast Abrade, target doesn't matter" $ do
+    tapForMana "R" "Cultivator's Caravan"
+    tapForMana "2" "Powerstone Shard 2"
+    castWithTriggers "1R" "Abrade" >> resolveTop
+
+  step "Activate Aetherflux Reservoir, targeting opponent" $ do
+    activate "" "Aetherflux Reservoir"
+    loseLife Active 50
+    damage (const 50) (targetPlayer Opponent) "Aetherflux Reservoir"
+    validateLife Opponent 0
+
+matchPowerstones = matchName "Powerstone Shard 1"
+                    `matchOr` matchName "Powerstone Shard 2"
+                   <> matchInPlay
+                   <> matchController Active
+
+matchArtifactMana = matchName "Mox Amber 1"
+                    `matchOr` matchName "Mox Amber 2"
+                    `matchOr` matchName "Cultivator's Caravan"
+                    `matchOr` matchName "Treasure"
+
+attributes = attributeFormatter $ do
+  attribute "our life" $ countLife Active
+  attribute "op. life" $ countLife Opponent
+  attribute "spells" $ countValue spellCount
+  attribute "mana" $ do
+    normal <- (+)
+                <$> countCards
+                  ( matchAttribute "land"
+                    `matchOr` matchArtifactMana
+                  <> missingAttribute tapped
+                  <> matchInPlay
+                  <> matchController Active
+                  )
+                <*> countManaPool Active
+    powerstones <- countCards matchPowerstones
+    untapped    <- countCards $ matchPowerstones <> missingAttribute tapped
+    return $ normal + (powerstones * untapped)
+
+manaSources = cardFormatter
+  "open mana sources"
+  ( matchAttribute "land"
+    `matchOr` matchArtifactMana
+    `matchOr` matchPowerstones
+  <> missingAttribute tapped
+  <> matchInPlay
+  <> matchController Active
+  )
+formatter 1 = attributes <> boardFormatter
+formatter _ = attributes <> manaSources
diff --git a/src/Solutions/Dominaria5.hs b/src/Solutions/Dominaria5.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/Dominaria5.hs
@@ -0,0 +1,106 @@
+module Solutions.Dominaria5 where
+
+import Dovin.V1
+import Dovin.Prelude
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 8
+    withLocation (Active, Hand) $ do
+      addPlaneswalker 5 "Karn, Scion of Urza 2"
+
+    withLocation (Active, Play) $ do
+      addPlaneswalker 2 "Karn, Scion of Urza 1"
+      addCreature (3, 3) "Weldfast Wingsmith"
+      withAttribute doublestrike $
+        addCreature (2, 2) "Storm Fleet Swashbuckler"
+      addCreature (1, 3) "Reckless Fireweaver"
+
+      addLands 3 "Sulfur Falls"
+      addLands 3 "Canyon Slough"
+
+    withLocation (Active, Exile) $ do
+      addInstant "Fatal Push"
+      addSorcery "Mutiny"
+
+    withLocation (Opponent, Play) $ do
+      addCreature (2, 3) "Aerial Responder 1"
+      addCreature (2, 3) "Aerial Responder 2"
+      addCreature (5, 5) "Bonded Horncrest"
+
+  step "Activate Karn to return Mutiny" $ do
+    activatePlaneswalker (-1) "Karn, Scion of Urza 1"
+    moveTo Hand "Mutiny"
+
+  step "Cast Mutiny, using Horncrest to destroy a Responder" $ do
+    tapForMana "R" "Sulfur Falls 1"
+    cast "R" "Mutiny" >> resolveTop
+    target "Bonded Horncrest"
+    target "Aerial Responder 1"
+    damage (view cardPower) (targetCard "Aerial Responder 1") "Bonded Horncrest"
+
+  step "Cast Karn, using legend rule to remove the existing one" $ do
+    tapForMana "U" "Sulfur Falls 2"
+    tapForMana "U" "Sulfur Falls 3"
+    tapForMana "B" "Canyon Slough 1"
+    tapForMana "B" "Canyon Slough 2"
+    cast "4" "Karn, Scion of Urza 2" >> resolveTop
+    moveTo Graveyard "Karn, Scion of Urza 1"
+
+  step "Activate Karn to return Fatal Push" $ do
+    activatePlaneswalker (-1) "Karn, Scion of Urza 2"
+    moveTo Hand "Fatal Push"
+
+  step "Cast Fatal Push destroying remaining Responder with Revolt from first Karn" $ do
+    tapForMana "B" "Canyon Slough 3"
+    cast "B" "Fatal Push" >> resolveTop
+    target "Aerial Responder 2"
+    destroy "Aerial Responder 2"
+
+  step "Attack with all for lethal, since Horncrest can't block alone" $ do
+    validate "Aerial Responder 1" $ invert matchInPlay
+    validate "Aerial Responder 2" $ invert matchInPlay
+
+    attackWith
+      [ "Weldfast Wingsmith"
+      , "Storm Fleet Swashbuckler"
+      , "Reckless Fireweaver"
+      ]
+
+    forCards
+      (matchAttributes [attacking, doublestrike])
+      (combatDamage [])
+
+    forCards
+      (matchAttributes [attacking])
+      (combatDamage [])
+
+    validateLife Opponent 0
+
+attributes = attributeFormatter $ do
+  attribute "life" $ countLife Opponent
+  attribute "mana" $
+    (+) <$> countCards
+              ( matchAttribute "land"
+              <> missingAttribute "tapped"
+              <> matchController Active
+              )
+        <*> countManaPool Active
+formatter 1 = boardFormatter
+formatter 3 = attributes
+  <> cardFormatter
+       "remaining creatures"
+       (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 6 = attributes
+  <> cardFormatter
+       "remaining creatures"
+       (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 7 = attributes
+  <> cardFormatter
+      "unblocked creatures"
+      (matchLocation (Active, Play)
+      <> matchAttribute creature
+      <> invert (matchAttribute "blocked")
+      )
+formatter _ = attributes
diff --git a/src/Solutions/Example.hs b/src/Solutions/Example.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/Example.hs
@@ -0,0 +1,41 @@
+module Solutions.Example where
+
+import Dovin
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 3
+
+    withLocation Hand $ addInstant "Plummet"
+    withLocation Play $ do
+      addLands 2 "Forest"
+
+    as Opponent $ do
+      withLocation Play $ do
+        withAttributes [flying, token] $ addCreature (4, 4) "Angel"
+        withAttributes [flying]
+          $ withEffect
+              matchInPlay
+              (matchOtherCreatures <> (const $ matchAttribute creature))
+              (pure . setAttribute hexproof)
+          $ addCreature (3, 4) "Shalai, Voice of Plenty"
+
+  step "Plummet to destroy Shalai" $ do
+    tapForMana "G" (numbered 1 "Forest")
+    tapForMana "G" (numbered 2 "Forest")
+    cast "1G" "Plummet"
+    resolve "Plummet"
+    with "Shalai, Voice of Plenty" $ \enemy -> do
+      target enemy
+      validate (matchAttribute flying) enemy
+      destroy enemy
+
+formatter :: Int -> Formatter
+formatter 2 = manaFormatter
+  <> cardFormatter "opponent creatures" (matchLocation (Opponent, Play))
+formatter _ = boardFormatter
+
+manaFormatter = attributeFormatter $ do
+  attribute "availble mana" $
+    countCards (matchAttribute land <> missingAttribute tapped)
diff --git a/src/Solutions/ExplorersOfIxalanContest.hs b/src/Solutions/ExplorersOfIxalanContest.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/ExplorersOfIxalanContest.hs
@@ -0,0 +1,192 @@
+module Solutions.ExplorersOfIxalanContest where
+
+import Dovin.V1
+import Dovin.Prelude
+
+-- This solution is not optimal, 130 damage is possible.
+solution :: GameMonad ()
+solution = do
+  let goblin = "goblin"
+  let pirate = "pirate"
+  let lazav = "Lazav, the Multifarious"
+  let shapeshift x = do
+        activate "" lazav
+        targetInLocation (Active, Graveyard) "Adanto Vanguard"
+
+  let goblinToken = withLocation (Active, Play)
+        . withAttributes [token, goblin]
+        . addCreature (1, 1)
+
+  step "Relevant initial state" $ do
+    withLocation (Active, Hand) $ do
+      withAttribute goblin $ addCreature (2, 2) "Legion Warboss"
+      withAttribute doublestrike
+        $ withEffect
+            matchInPlay
+            (matchOtherCreatures <> (const $ matchAttribute firststrike))
+            (pure . setAttribute doublestrike)
+        $ addCreature (2, 2) "Kwende, Pride of Femeref"
+
+      addSorcery "Switcheroo"
+      addInstant "Buccaneer's Bravado"
+
+    withLocation (Active, Play) $ do
+      addCreature (1, 3) lazav
+      withAttributes [goblin, token] $ addCreature (1, 1) "Goblin 1"
+      withAttributes [goblin, token] $ addCreature (1, 1) "Goblin 2"
+
+    withLocation (Active, Graveyard) $ do
+      addCreature (1, 1) "Adanto Vanguard"
+      addCreature (1, 3) "Lazav, the Multifarious 2"
+      withAttribute deathtouch $ addCreature (3, 3) "Isareth the Awakener"
+      addCreature (4, 3) "Truefire Captain"
+      withAttribute goblin $ addCreature (2, 2) "Siege-Gang Commander"
+      withAttribute deathtouch $ addCreature (1, 1) "Ochran Assassin"
+
+    withLocation (Opponent, Play) $ do
+      withAttributes [indestructible, doublestrike] $
+        addCreature (4, 8) "Zetalpa, Primal Dawn"
+      withAttribute pirate $ addCreature (4, 4) "Angrath's Marauders"
+      withAttribute firststrike $ addCreature (3, 3) "Goblin Chainwhirler"
+      withEffect
+        matchInPlay
+        matchOtherCreatures
+        (pure . setAttribute haste)
+        $ addCreature (3, 3) "Garna, the Bloodflame"
+
+  step "Cast Legion Warboss and Kwende from hand" $ do
+    cast "" "Legion Warboss"
+    resolve "Legion Warboss"
+    cast "" "Kwende, Pride of Femeref"
+    resolve "Kwende, Pride of Femeref"
+
+  step "Buccaneer's Bravado on Angrath's, giving first strike and +1/+1" $ do
+    with "Angrath's Marauders" $ \x -> do
+      cast "" "Buccaneer's Bravado"
+      target x
+      validate x $ matchAttribute pirate
+      resolve "Buccaneer's Bravado"
+
+      modifyStrength (1, 1) x
+      gainAttribute firststrike x
+
+  step "Switcheroo Kwende and Garna, creatures get haste and doublestrike appropriately" $ do
+    cast "" "Switcheroo"
+    target "Kwende, Pride of Femeref"
+    target "Garna, the Bloodflame"
+    resolve "Switcheroo"
+
+    move (Active, Play) (Opponent, Play) "Kwende, Pride of Femeref"
+    move (Opponent, Play) (Active, Play) "Garna, the Bloodflame"
+
+    gainAttribute summoned "Kwende, Pride of Femeref"
+    gainAttribute summoned "Garna, the Bloodflame"
+
+  step "Shapeshift to Adanto Vanguard and make indestructible" $ do
+    shapeshift "Adanto Vanguard"
+    activate "" lazav
+    gainAttribute indestructible lazav
+
+  step "Shapeshift Lazav to Isareth" $ do
+    shapeshift "Isareth the Awakener"
+
+  step "Begin combat, create a new goblin token from Warboss" $ do
+    trigger "Legion Warboss"
+    withAttribute haste $ goblinToken "Goblin 3"
+
+  step "Attack with lazav and all goblins (haste from Garna), with mentor from Warboss" $ do
+    attackWith [lazav, "Legion Warboss", "Goblin 1", "Goblin 2", "Goblin 3"]
+
+    triggerMentor "Legion Warboss" "Goblin 1"
+
+  step "Trigger lazav-as-isareth, reanimating Seige-Gang Commander" $ do
+    trigger lazav
+    targetInLocation (Active, Graveyard) "Siege-Gang Commander"
+    move (Active, Graveyard) (Active, Play) "Siege-Gang Commander"
+
+    -- haste from Garna, even though not relevant
+    forM_ [4..6] $ \n -> withAttribute haste $ goblinToken (numbered n "Goblin")
+
+  step "After declare attacker, shapeshift to Ochran Assassin, luring all enemies to block" $ do
+    shapeshift "Ochran Assassin"
+    loseAttribute deathtouch lazav -- From Isareth
+    gainAttribute deathtouch lazav -- From Assassin
+
+    forCards
+      (matchLocation (Opponent, Play))
+      (gainAttribute "blocking")
+    gainAttribute "blocked" lazav
+
+  step "After declare blockers, shapeshift to Truefire Captain" $ do
+    shapeshift "Truefire Captain"
+    loseAttribute deathtouch lazav -- From Assassin
+
+  step "First strike damage from enemies to lazav, doubled from Angrath's, bounced to opponent from Truefire" $ do
+    forCards
+      (    matchLocation (Opponent, Play)
+        <> matchAttribute "blocking"
+        <> (matchAttribute firststrike `matchOr` matchAttribute doublestrike)
+      )
+      $ \cn -> do
+        damage ((* 2) . view cardPower) (targetCard lazav) cn
+        damage ((* 2) . view cardPower) (targetPlayer Opponent) cn
+
+  step "Regular damage from enemies to lazav, doubled from Angrath's, bounced to opponent from Truefire" $ do
+    forCards (matchLocation (Opponent, Play) <> matchAttribute "blocking")
+      $ \cn -> do
+        damage ((* 2) . view cardPower) (targetCard lazav) cn
+        damage (view cardPower) (targetCard cn) lazav
+        damage ((* 2) . view cardPower) (targetPlayer Opponent) cn
+
+  step "Regular damage from attackers to player" $ do
+    forCards
+      (matchLocation (Active, Play) <> matchAttribute attacking <> missingAttribute "blocked")
+      (combatDamage [])
+
+  let sacrificeToSiegeGang = \name -> do
+        activate "" "Siege-Gang Commander"
+        validate name $ matchAttribute goblin
+        sacrifice name
+        damage (const 2) (targetPlayer Opponent) "Siege-Gang Commander"
+
+  step "Siege-gang all the goblins except Siege-Gang" $ do
+    commander <- requireCard "Siege-Gang Commander" mempty
+
+    forCards
+      ((invert . matchName) "Siege-Gang Commander" <> matchAttribute goblin)
+      sacrificeToSiegeGang
+
+  step "Shapeshift to Warboss, sacrifice lazav and self to Siege-Gang" $ do
+    shapeshift "Legion Warboss"
+    gainAttribute goblin lazav
+
+    sacrificeToSiegeGang lazav
+    sacrificeToSiegeGang "Siege-Gang Commander"
+
+damageFormatter = attributeFormatter $ do
+  attribute "cumulative damage" $ (* (-1)) <$> countLife Opponent
+
+formatter :: Int -> Formatter
+formatter 1 =
+     cardFormatter "hand" (matchLocation (Active, Hand))
+  <> cardFormatter "our creatures" (matchLocation (Active, Play))
+  <> cardFormatter "opponent creatures" (matchLocation (Opponent, Play))
+  <> cardFormatter "graveyard" (matchLocation (Active, Graveyard))
+formatter 2 = cardFormatter "our creatures" (matchLocation (Active, Play))
+formatter 8 = cardFormatter "attacking creatures" (matchAttribute "attacking")
+formatter 9 = cardFormatter "our creatures" (matchLocation (Active, Play))
+formatter 12 = damageFormatter <>
+  cardFormatter
+   "blocking creatures with doublestrike"
+   (matchAttribute "blocking" <> matchAttribute doublestrike)
+formatter 13 = damageFormatter <>
+  cardFormatter "blocking creatures" (matchAttribute "blocking")
+formatter 14 = damageFormatter <>
+  cardFormatter
+    "unblocked creatures"
+    (matchAttribute "attacking" <> missingAttribute "blocked")
+formatter 15 = damageFormatter <>
+  cardFormatter "remaining creatures" (matchLocation (Active, Play))
+formatter 16 = damageFormatter
+
+formatter _ = blankFormatter
diff --git a/src/Solutions/GuildsOfRavnica1.hs b/src/Solutions/GuildsOfRavnica1.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/GuildsOfRavnica1.hs
@@ -0,0 +1,61 @@
+module Solutions.GuildsOfRavnica1 where
+
+import Control.Monad (forM_)
+
+import Dovin.V1
+
+-- http://www.possibilitystorm.com/083-guilds-of-ravnica-puzzle-1/
+solution :: GameMonad ()
+solution = do
+  let mentor = "mentor"
+
+  step "Initial state" $ do
+    setLife Opponent 5
+
+    withLocation (Active, Hand)
+      $ withAttributes [flying, mentor]
+      $ addCreature (2, 5) "Aurelia, Exemplar of Justice"
+
+    withLocation (Active, Play) $ do
+      withAttribute mentor $ do
+        addCreature (3, 1) "Blade Instructor"
+        addCreature (1, 1) "Goblin Banneret"
+        addCreature (4, 2) "Barging Sergeant"
+      addPlaneswalker 5 "Angrath, the Flame-Chained"
+
+      addLands 4 "Sacred Foundry"
+      addLands 4 "Dragonskull Summit"
+
+  step "Cast Aurelia" $ do
+    tapForMana "R" "Sacred Foundry 1"
+    tapForMana "W" "Sacred Foundry 2"
+    tapForMana "W" "Sacred Foundry 3"
+    tapForMana "W" "Sacred Foundry 4"
+    cast "2RW" "Aurelia, Exemplar of Justice"
+    resolve "Aurelia, Exemplar of Justice"
+
+  step "Angrath gain control, targeting Aurelia" $ do
+    activatePlaneswalker (-3) "Angrath, the Flame-Chained"
+    target "Aurelia, Exemplar of Justice"
+    gainAttribute "haste" "Aurelia, Exemplar of Justice"
+
+  step "Activate Goblin Banneret" $ do
+    forM_ [1..2] $ \n -> tapForMana "R" (numbered n "Dragonskull Summit")
+    activate "R1" "Goblin Banneret"
+    modifyStrength (2, 0) "Goblin Banneret"
+
+  step "Begin combat, put Aurelia's trigger on Banneret" $ do
+    trigger "Aurelia, Exemplar of Justice"
+    modifyStrength (2, 0) "Goblin Banneret"
+
+  step "Attack with everything, stacking Mentor triggers on to Aurelia" $ do
+    attackWith ["Aurelia, Exemplar of Justice", "Blade Instructor", "Goblin Banneret", "Barging Sergeant"]
+    triggerMentor "Blade Instructor" "Aurelia, Exemplar of Justice"
+    triggerMentor "Barging Sergeant" "Aurelia, Exemplar of Justice"
+    triggerMentor "Goblin Banneret" "Aurelia, Exemplar of Justice"
+
+    combatDamage [] "Aurelia, Exemplar of Justice"
+
+    validateLife Opponent 0
+
+formatter _ = boardFormatter
diff --git a/src/Solutions/GuildsOfRavnica3.hs b/src/Solutions/GuildsOfRavnica3.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/GuildsOfRavnica3.hs
@@ -0,0 +1,143 @@
+module Solutions.GuildsOfRavnica3 where
+
+import Control.Monad
+
+import Dovin.V1
+
+-- This solution re-uses the "Treasure" card to avoid having to track a counter
+-- for each new one created. This has the downside of requiring explicit
+-- state-based action calls - a new one can't be created until the old one has
+-- been removed. In hindsight, probably would be easier to follow by keeping a
+-- running counter of treasures and refering to them separately.
+solution :: GameMonad ()
+solution = do
+  let menace = "menace"
+  let sacrificeToNecrolisk =
+        \name -> do
+          validateCanCastSorcery
+          activate "1" "Undercity Necrolisk"
+          validate name $
+               matchInPlay
+            <> matchController Active
+            <> matchAttribute "creature"
+          sacrifice name
+          gainAttribute menace "Undercity Necrolisk"
+          modifyStrength (1, 1) "Undercity Necrolisk"
+          whenMatch "Pitiless Plunderer" matchInPlay $ do
+            trigger "Pitiless Plunderer"
+            withLocation (Active, Play)
+              $ withAttribute token
+              $ addArtifact "Treasure"
+
+  step "Initial state" $ do
+    setLife Opponent 9
+
+    withLocation (Active, Hand) $ do
+      withAttribute lifelink $ addCreature (1, 1) "Hunted Witness"
+      addCreature (8, 5) "Silverclad Ferocidons"
+      addInstant "Justice Strike"
+
+    withLocation (Active, Play) $ do
+      withAttribute menace $ addCreature (9, 3) "Roc Charger"
+      addArtifact "Desecrated Tomb"
+      addCreature (3, 3) "Undercity Necrolisk"
+      addCreature (1, 4) "Pitiless Plunderer"
+      addCreature (2, 2) "Oathsworn Vampire"
+      forM_ [1..4] $ \n -> do
+        addLand (numbered n "Boros Guildgate")
+        addLand (numbered n "Gateway Plaza")
+
+    withLocation (Opponent, Play) $ do
+      addCreature (4, 3) "Rekindling Phoenix 1"
+      addCreature (4, 3) "Rekindling Phoenix 2"
+      addCreature (4, 3) "Aurelia, Exemplar of Justice"
+
+  step "Cast Hunted Witness and sac it" $ do
+    tapForMana "W" "Boros Guildgate 1"
+    cast "W" "Hunted Witness"
+    resolve "Hunted Witness"
+
+    tapForMana "W" "Boros Guildgate 2"
+    sacrificeToNecrolisk "Hunted Witness"
+    withLocation (Active, Play)
+      $ withAttributes [lifelink, token]
+      $ addCreature (1, 1) "Soldier"
+
+  step "Sac Oathsworn Vampire" $ do
+    withStateBasedActions $ do
+      tapForMana "1" "Treasure"
+      sacrifice "Treasure"
+    sacrificeToNecrolisk "Oathsworn Vampire"
+
+  step "Justice Strike soldier to trigger life gain" $ do
+    tapForMana "W" "Treasure"
+    sacrifice "Treasure"
+    tapForMana "R" "Boros Guildgate 3"
+
+    cast "RW" "Justice Strike"
+    resolve "Justice Strike"
+    target "Soldier"
+    fight "Soldier" "Soldier"
+
+  step "Cast Oathsworn Vampire from Graveyard, triggering Desecrated Tomb" $ do
+    tapForMana "R" "Boros Guildgate 4"
+    tapForMana "B" "Gateway Plaza 1"
+    castFromLocation (Active, Graveyard) "1B" "Oathsworn Vampire"
+    resolve "Oathsworn Vampire"
+
+    trigger "Desecrated Tomb"
+    withLocation (Active, Play)
+      $ withAttributes [flying, token]
+      $ addCreature (1, 1) "Bat"
+
+  step "Sac vampire, bat, and plunderer" $ do
+    tapForMana "B" "Gateway Plaza 2"
+    sacrificeToNecrolisk "Oathsworn Vampire"
+
+    withStateBasedActions $ do
+      tapForMana "1" "Treasure"
+      sacrifice "Treasure"
+    sacrificeToNecrolisk "Bat"
+
+  step "Repeat vampire/bat cycle" $ do
+    withStateBasedActions $ do
+      tapForMana "B" "Gateway Plaza 3"
+      tapForMana "1" "Treasure"
+      sacrifice "Treasure"
+
+    castFromLocation (Active, Graveyard) "1B" "Oathsworn Vampire"
+    resolve "Oathsworn Vampire"
+
+    trigger "Desecrated Tomb"
+    withLocation (Active, Play)
+      $ withAttributes [flying, token]
+      $ addCreature (1, 1) "Bat"
+
+    tapForMana "B" "Gateway Plaza 4"
+    sacrificeToNecrolisk "Oathsworn Vampire"
+
+    withStateBasedActions $ do
+      tapForMana "1" "Treasure"
+      sacrifice "Treasure"
+    sacrificeToNecrolisk "Bat"
+
+  step "Attack with Roc and Necrolisk" $ do
+    validate "Roc Charger" $ matchAttribute "menace"
+    validate "Undercity Necrolisk" $ matchAttribute "menace"
+
+    attackWith ["Roc Charger", "Undercity Necrolisk"]
+
+  let blockers = ["Rekindling Phoenix 1", "Rekindling Phoenix 2"]
+
+  fork $
+    [ step "Roc is blocked" $ do
+        combatDamage blockers "Roc Charger"
+        combatDamage [] "Undercity Necrolisk"
+        validateLife Opponent 0
+    , step "Undercity Necrolisk is blocked" $ do
+        combatDamage [] "Roc Charger"
+        combatDamage blockers "Undercity Necrolisk"
+        validateLife Opponent 0
+    ]
+
+formatter _ = boardFormatter
diff --git a/src/Solutions/GuildsOfRavnica8.hs b/src/Solutions/GuildsOfRavnica8.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/GuildsOfRavnica8.hs
@@ -0,0 +1,141 @@
+module Solutions.GuildsOfRavnica8 where
+
+import Control.Monad.Except (throwError, when)
+import Control.Lens
+import qualified Data.Set as S
+
+import Dovin.V1
+
+-- http://www.possibilitystorm.com/089-guilds-of-ravnica-season-puzzle-7-2/
+solution :: GameMonad ()
+solution = do
+  let black = "black"
+
+  -- This solutions relies on triggering Diamond Mare to gain life, which in
+  -- turns triggers Epicure of Blood to cause the opponent to lose life. This
+  -- helper can wrap cast actions with that combination.
+  let withTriggers = \action name -> do
+        action name
+        trigger "Diamond Mare"
+        c <- requireCard name mempty
+
+        when (hasAttribute black c) $ do
+          gainLife Active 1
+          trigger "Epicure of Blood"
+          loseLife Opponent 1
+
+
+  -- Helper function to keep track of which permanent types have been cast
+  -- using Muldrotha's ability.
+  let castWithMuldrotha = \ptype mana cn -> do
+        let ptypes = S.fromList ["artifact", "creature", "land", "enchantment"]
+        let counterName = "muldrotha-" <> ptype
+
+        when (not $ S.member ptype ptypes) $
+          throwError $ "Invalid permanent type: " <> ptype
+
+        n <- use (counters . at counterName . non 0)
+
+        if n > 0 then
+          throwError $ "Already cast card of type with Muldrotha: " <> ptype
+        else
+          do
+            castFromLocation (Active, Graveyard) mana cn
+            resolve cn
+            assign (counters . at counterName) (Just 1)
+
+  step "Initial state" $ do
+    setLife Opponent 7
+
+    withLocation (Active, Play) $ do
+      addCreature (4, 4) "Epicure of Blood"
+      addCreature (6, 6) "Muldrotha, the Gravetide"
+
+      addLands 3 "Memorial to Folly"
+      addLands 4 "Watery Grave"
+      addLands 4 "Overgrown Tomb"
+
+    withLocation (Active, Graveyard) $ do
+      withAttribute artifact $ addCreature (1, 3) "Diamond Mare"
+      addLand "Detection Tower"
+      addArtifact "Mox Amber"
+      withAttribute black $ addCreature (1, 2) "Vicious Conquistador"
+      addCreature (1, 4) "Sailor of Means"
+
+    withLocation (Active, Hand) $ withAttribute black $ do
+      addSorcery "March of the Drowned"
+      addSorcery "Gruesome Menagerie"
+      addAura "Dead Weight"
+      addSorcery "Find"
+
+  step "Detection Tower, Mox Amber, Diamond Mare from graveyard" $ do
+    castWithMuldrotha "land" "" "Detection Tower"
+    castWithMuldrotha "artifact" "" "Mox Amber"
+    tapForMana "1" "Detection Tower"
+    tapForMana "1" "Mox Amber"
+    castWithMuldrotha "creature" "2" "Diamond Mare"
+
+  step "March of the Drowned on Vicious Conquistador" $ do
+    tapForMana "B" "Memorial to Folly 1"
+    withTriggers (cast "B") "March of the Drowned"
+    resolve "March of the Drowned"
+    returnToHand "Vicious Conquistador"
+
+  step "Vicious Conquistador" $ do
+    tapForMana "B" "Memorial to Folly 2"
+    withTriggers (cast "B") "Vicious Conquistador"
+    resolve "Vicious Conquistador"
+
+  step "Dead Weight on Vicious Conquistador" $ do
+    tapForMana "B" "Memorial to Folly 3"
+    withTriggers (cast "B") "Dead Weight"
+    target "Vicious Conquistador"
+    resolve "Dead Weight"
+    modifyStrength (-2, -2) "Vicious Conquistador"
+    resetStrength "Vicious Conquistador" (1, 2)
+    moveTo Graveyard "Dead Weight"
+
+  step "Gruesome Menagerie for Sailor of Means and Vicious Conquistador" $ do
+    tapForMana "B" "Watery Grave 1"
+    tapForMana "B" "Watery Grave 2"
+    tapForMana "B" "Watery Grave 3"
+    tapForMana "B" "Watery Grave 4"
+    tapForMana "B" "Overgrown Tomb 1"
+    withTriggers (cast "3BB") "Gruesome Menagerie"
+    resolve "Gruesome Menagerie"
+    targetInLocation (Active, Graveyard) "Vicious Conquistador"
+    targetInLocation (Active, Graveyard) "Sailor of Means"
+    returnToPlay "Vicious Conquistador"
+    returnToPlay "Sailor of Means"
+    withLocation (Active, Play)
+      $ withAttribute token
+      $ addArtifact "Treasure"
+
+  step "Dead Weight on Vicious Conquistador" $ do
+    tapForMana "B" "Overgrown Tomb 2"
+    withTriggers (castWithMuldrotha "enchantment" "B") "Dead Weight"
+    target "Vicious Conquistador"
+    modifyStrength (-2, -2) "Vicious Conquistador"
+    resetStrength "Vicious Conquistador" (1, 2)
+    moveTo Graveyard "Dead Weight"
+
+  step "Find for Vicous Conquistador" $ do
+    tapForMana "B" "Overgrown Tomb 3"
+    tapForMana "B" "Overgrown Tomb 4"
+    withTriggers (cast "BB") "Find"
+    resolve "Find"
+    targetInLocation (Active, Graveyard) "Vicious Conquistador"
+    returnToHand "Vicious Conquistador"
+
+  step "Vicious Conquistador" $ do
+    tapForMana "B" "Treasure"
+    sacrifice "Treasure"
+    withTriggers (cast "B") "Vicious Conquistador"
+    resolve "Vicious Conquistador"
+
+    validateLife Opponent 0
+
+formatter :: Int -> Formatter
+formatter _ = attributeFormatter $ do
+  attribute "mana" $ countCards (matchAttribute "land" <> missingAttribute "tapped")
+  attribute "life" $ countLife Opponent
diff --git a/src/Solutions/GuildsOfRavnica9.hs b/src/Solutions/GuildsOfRavnica9.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/GuildsOfRavnica9.hs
@@ -0,0 +1,202 @@
+module Solutions.GuildsOfRavnica9 where
+
+import Control.Lens
+import Control.Monad
+
+import Dovin.V1
+
+solution :: GameMonad ()
+solution = do
+  -- This puzzle relies heavily on casting triggers, so wrap the relevant ones
+  -- up in this helper.
+  --
+  -- For ease of use, spells that will be copied are named with a trailing " 1"
+  -- and subsequent copies increment this number.
+  let withTriggers = \action name -> do
+        action name
+        trigger "Thousand-Year Storm"
+        triggerStorm $
+          \n -> copySpell name
+                  (numbered (n + 1) (zipWith const name (drop 2 name)))
+
+        trigger "Adeliz, the Cinder Wind"
+        modifyStrength (1, 1) "Adeliz, the Cinder Wind"
+
+  -- We'll be making a lot of archers...
+  let addArcherCopy name = do
+        withLocation (Active, Play) $
+          withAttributes [token, summoned] $ addCreature (1, 4) name
+
+  let angel = "angel"
+  let merfolk = "merfolk"
+
+  step "Initial state" $ do
+    setLife Opponent 12
+
+    withLocation (Active, Hand) $ do
+      addSorcery "Undercity Uprising"
+      addSorcery "Doublecast 1"
+      addInstant "Plummet 1"
+      addSorcery "Quasiduplicate 1"
+      withAttribute flying $ addCreature (7, 6) "Torgaar, Famine Incarnate"
+      addAura "Waterknot"
+
+    withLocation (Active, Play) $ do
+      addEnchantment "Thousand-Year Storm"
+      -- Has +2/+2 from Maniacal Rage aura
+      withAttribute flying $ addCreature (4, 4) "Adeliz, the Cinder Wind"
+      addCreature (1, 4) "Afzocan Archer"
+
+      addLands 4 "Timber Gorge"
+      addLands 4 "Submerged Boneyard"
+      addLands 4 "Highland Lake"
+
+    withLocation (Opponent, Play) $ do
+      withAttribute "merfolk" $ addCreature (2, 2) "Kopala, Warden of Waves"
+      withAttributes [flying, token] $ addCreature (4, 4) "Angel 1"
+      withAttributes [flying, token] $ addCreature (4, 4) "Angel 2"
+      withAttributes [flying, token] $ addCreature (4, 4) "Angel 3"
+
+      withAttributes [flying, angel]
+        $ withEffect
+            matchInPlay
+            matchOtherCreatures
+            (pure . setAttribute hexproof)
+        $ addCreature (3, 4) "Shalai, Voice of Plenty"
+
+      withAttributes [flying, lifelink, angel]
+        $ withEffect
+            matchInPlay
+            (matchOtherCreatures <> (const $ matchAttribute angel))
+            (pure . over cardStrength (mkStrength (1, 1) <>) . setAttribute lifelink)
+        $ addCreature (4, 4) "Lyra Dawnbringer"
+
+      withAttribute merfolk
+        $ withEffect
+            matchInPlay
+            (matchOtherCreatures <> (const $ matchAttribute merfolk))
+            (pure . over cardStrength (mkStrength (1, 1) <>))
+        $ addCreature (2, 2) "Merfolk Mistbinder 1"
+
+      withAttribute merfolk
+        $ withEffect
+            matchInPlay
+            (matchOtherCreatures <> (const $ matchAttribute merfolk))
+            (pure . over cardStrength (mkStrength (1, 1) <>))
+        $ addCreature (3, 3) "Merfolk Mistbinder 2"
+
+  step "Use Undercity Uprising on Adeliz to destroy Shalai" $ do
+    tapForMana "G" (numbered 1 "Timber Gorge")
+    tapForMana "B" (numbered 1 "Submerged Boneyard")
+    tapForMana "B" (numbered 2 "Submerged Boneyard")
+
+    withTriggers (cast "1GB") "Undercity Uprising"
+    resolve "Undercity Uprising"
+    forCards
+      (matchAttribute creature <> matchLocation (Active, Play))
+      (gainAttribute deathtouch)
+
+    with "Shalai, Voice of Plenty" $ \enemy -> do
+      fight "Adeliz, the Cinder Wind" enemy
+      validate enemy $ matchLocation (Opponent, Graveyard)
+
+  step "Cast Doublecast" $ do
+    tapForMana "R" (numbered 2 "Timber Gorge")
+    tapForMana "R" (numbered 3 "Timber Gorge")
+    withTriggers (cast "RR") "Doublecast 1"
+
+    resolve "Doublecast 2"
+    resolve "Doublecast 1"
+
+  step "Cast Plummet to destroy all fliers" $ do
+    tapForMana "G" "Timber Gorge 4"
+    withTriggers (cast "G") "Plummet 1"
+
+    -- From double doublecast earlier
+    copySpell "Plummet 1" "Plummet 4"
+    copySpell "Plummet 1" "Plummet 5"
+
+    resolve "Plummet 5"
+    with "Lyra Dawnbringer" $ \enemy -> do
+      target enemy
+      validate enemy $ matchAttribute flying
+      destroy enemy
+      validate enemy $ matchLocation (Opponent, Graveyard)
+
+    forM_ [1..3] $ \n -> do
+      resolve (numbered (5 - n) "Plummet")
+      with (numbered n "Angel") $ \enemy -> do
+        target enemy
+        validate enemy $ matchAttribute flying
+        destroy enemy
+
+    resolve "Plummet 1" -- No target
+
+  step "Quasiduplicate on archer, destroy one of the Mistbinders" $ do
+    tapForMana "U" (numbered 1 "Highland Lake")
+    tapForMana "U" (numbered 2 "Highland Lake")
+    withTriggers (cast "UU") "Quasiduplicate 1"
+
+    with ("Merfolk Mistbinder 2") $ \enemy -> do
+      forM_ [1..4] $ \n -> do
+        let tokenName = ("Afzocan Archer " <> show n)
+        resolve $ numbered (5 - n) "Quasiduplicate"
+        addArcherCopy tokenName
+        fight tokenName enemy
+
+      validate enemy $ matchLocation (Opponent, Graveyard)
+
+  step "Jump-start Quasiduplicate again (w/ Waterknot), destroy merfolk" $ do
+    tapForMana "U" (numbered 3 "Highland Lake")
+    tapForMana "U" (numbered 4 "Highland Lake")
+    withTriggers (jumpstart "UU" "Waterknot") "Quasiduplicate 1"
+
+    with (numbered 1 "Merfolk Mistbinder") $ \enemy -> do
+      forM_ [1..2] $ \n -> do
+        let tokenName = ("Afzocan Archer " <> show n)
+        resolve $ numbered (6 - n) "Quasiduplicate"
+        addArcherCopy tokenName
+        fight tokenName enemy
+
+      validate enemy $ matchLocation (Opponent, Graveyard)
+
+    with "Kopala, Warden of Waves" $ \enemy -> do
+      forM_ [3..4] $ \n -> do
+        let tokenName = numbered n "Afzocan Archer"
+        resolve $ numbered (6 - n) "Quasiduplicate"
+        addArcherCopy tokenName
+        fight tokenName enemy
+
+      validate enemy $ matchLocation (Opponent, Graveyard)
+
+    forM_ [5] $ \n -> do
+      let tokenName = numbered n "Afzocan Archer"
+      resolve $ numbered (6 - n) "Quasiduplicate"
+      addArcherCopy tokenName
+
+  step "Torgaar, sacrificing archers to reduce cost" $ do
+    tapForMana "B" (numbered 3 "Submerged Boneyard")
+    tapForMana "B" (numbered 4 "Submerged Boneyard")
+    sacrifice $ numbered 1 "Afzocan Archer"
+    sacrifice $ numbered 2 "Afzocan Archer"
+    sacrifice $ numbered 3 "Afzocan Archer"
+    cast "BB" "Torgaar, Famine Incarnate"
+    resolve "Torgaar, Famine Incarnate"
+    setLife Opponent 10
+
+  step "Attack with Adeliz and initial archer for lethal" $ do
+    attackWith ["Adeliz, the Cinder Wind", "Afzocan Archer"]
+
+    combatDamage [] "Adeliz, the Cinder Wind"
+    combatDamage [] "Afzocan Archer"
+
+    validateLife Opponent 0
+
+formatter :: Int -> Formatter
+formatter _ = attributeFormatter $ do
+  attribute "mana" $
+    countCards (matchAttribute "land" <> missingAttribute "tapped")
+  attribute "storm"  $ countValue "storm"
+  attribute "adeliz" $
+    view cardStrength <$> requireCard "Adeliz, the Cinder Wind" mempty
+  attribute "enemies" $ countCards (matchLocation (Opponent, Play))
diff --git a/src/Solutions/GuildsOfRavnicaPre2.hs b/src/Solutions/GuildsOfRavnicaPre2.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/GuildsOfRavnicaPre2.hs
@@ -0,0 +1,74 @@
+module Solutions.GuildsOfRavnicaPre2 where
+
+import Dovin.V1
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 9
+
+    withLocation (Active, Hand) $ do
+      addCreature (1, 1) "Ochran Assassin"
+      addCreature (2, 2) "Rhizome Lurcher"
+
+    withLocation (Active, Play) $ do
+      addCreature (1, 1) "Torch Courier"
+      withAttribute flying $ addCreature (3, 2) "Whisper Agent"
+      addCreature (2, 2) "Whisper, Blood Liturgist"
+
+      addLands 3 "Dragonskull Summit"
+      addLands 4 "Woodland Cemetery"
+
+    withLocation (Active, Graveyard) $ do
+      addCreature (2, 2) "Devkarin Dissident"
+      addCreature (4, 3) "Underrealm Lich"
+      addCreature (3, 4) "Golgari Findbroker"
+      addCreature (2, 2) "Erstwhile Trooper"
+      addCreature (5, 4) "Bone Dragon"
+
+  step "Play Ochran Assassin, haste with Torch Courier" $ do
+    tapForMana "G" "Woodland Cemetery 1"
+    tapForMana "B" "Woodland Cemetery 2"
+    tapForMana "R" "Dragonskull Summit 1"
+    cast "1BG" "Ochran Assassin"
+    resolve "Ochran Assassin"
+
+    activate "" "Torch Courier"
+    sacrifice "Torch Courier"
+
+    gainAttribute "haste" "Ochran Assassin"
+
+  step "Sac Whisper to get Torch Courier back" $ do
+    tap "Whisper, Blood Liturgist"
+    sacrifice "Whisper Agent"
+    sacrifice "Whisper, Blood Liturgist"
+
+    returnToPlay "Torch Courier"
+
+  step "Play Rhizome Lurcher, haste with Torch Courier" $ do
+    tapForMana "G" "Woodland Cemetery 3"
+    tapForMana "B" "Woodland Cemetery 4"
+    tapForMana "R" "Dragonskull Summit 2"
+    tapForMana "R" "Dragonskull Summit 3"
+    cast "2BG" "Rhizome Lurcher"
+    resolve "Rhizome Lurcher"
+
+    forCards
+      (matchLocation (Active, Graveyard) <> matchAttribute "creature")
+      (const $ modifyStrength (1, 1) "Rhizome Lurcher")
+
+    activate "" "Torch Courier"
+    sacrifice "Torch Courier"
+
+    gainAttribute "haste" "Rhizome Lurcher"
+
+  step "Attack with Lurcher and Assasin, everyone blocks Assasin" $ do
+    attackWith ["Rhizome Lurcher", "Ochran Assassin"]
+
+    gainAttribute "blocked" "Ochran Assassin"
+
+    combatDamage [] "Rhizome Lurcher"
+
+    validateLife Opponent 0
+
+formatter _ = boardFormatter
diff --git a/src/Solutions/RivalsOfIxalan7.hs b/src/Solutions/RivalsOfIxalan7.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/RivalsOfIxalan7.hs
@@ -0,0 +1,134 @@
+module Solutions.RivalsOfIxalan7 where
+
+import Dovin.Prelude
+import Dovin.V1
+
+blocked = "blocked"
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 7
+
+    withLocation (Active, Play) $ do
+      addLands 2 "Mountain"
+      addLands 2 "Plains"
+
+      withAttributes [trample] $ addCreature (5, 5) "Rowdy Crew"
+      addCreature (2, 2) "Needletooth Raptor"
+      addCreature (0, 1) "Tilonalli's Skinshifter"
+      withAttributes [flying]
+        $ withEffect
+            (matchInPlay <> matchAttribute exerted)
+            (    matchLocation . view cardLocation
+              <> const (matchAttribute creature)
+            )
+            (pure . over cardStrength (mkStrength (1, 1) <>))
+        $ addCreature (2, 2) "Tah-Crop Elite"
+
+    withLocation (Active, Hand) $ do
+      withAttribute haste $ addCreature (1, 1) "Fanatical Firebrand"
+      addInstant "Sure Strike"
+
+    withLocation (Opponent, Play) $ do
+      addLand "Spires of Orcaza"
+      addCreature (2, 2) "Aerial Responder"
+      addCreature (3, 5) "Bellowing Aegisaur 1"
+      addCreature (3, 5) "Bellowing Aegisaur 2"
+
+  step "Cast Firebrand" $ do
+    tapForMana "R" "Mountain 1"
+    cast "R" "Fanatical Firebrand" >> resolveTop
+
+  step "Activate Firebrand to damage raptor, killing Aerial Responder" $ do
+    activate "" "Fanatical Firebrand"
+    tap "Fanatical Firebrand"
+    sacrifice "Fanatical Firebrand"
+    target "Needletooth Raptor"
+
+    trigger "Needletooth Raptor"
+    damage (const 5) (targetCard "Aerial Responder") "Needletooth Raptor"
+
+  step "Attack with all, Skinshifter as Tah-Crop and exerting Tah-Crop" $ do
+    validate "Aerial Responder" $ invert matchInPlay
+
+    attackWith
+      [ "Tah-Crop Elite"
+      , "Rowdy Crew"
+      , "Needletooth Raptor"
+      , "Tilonalli's Skinshifter"
+      ]
+
+    exert "Tah-Crop Elite"
+
+    trigger "Tilonalli's Skinshifter"
+    target "Tah-Crop Elite"
+    validate "Tah-Crop Elite" $ matchAttribute attacking
+    resetStrength "Tilonalli's Skinshifter" (2, 2)
+    gainAttribute flying "Tilonalli's Skinshifter"
+
+  fork
+    [ step "No spire, block out ground damage" $ do
+        combatDamage [] "Tah-Crop Elite"
+        combatDamage [] "Tilonalli's Skinshifter"
+        combatDamage ["Bellowing Aegisaur 1"] "Rowdy Crew"
+        combatDamage ["Bellowing Aegisaur 2"] "Needletooth Raptor"
+
+        validateLife Opponent 0
+
+    , step "Spire one of the flyers, sure strike pushes through damage" $ do
+        tap "Spires of Orcaza"
+        untap "Tah-Crop Elite"
+        loseAttribute attacking "Tah-Crop Elite"
+
+        tapForMana "R" "Mountain 2"
+        tapForMana "W" "Plains 1"
+        cast "1R" "Sure Strike" >> resolveTop
+        target "Tilonalli's Skinshifter"
+        modifyStrength (3, 0) "Tilonalli's Skinshifter"
+
+        combatDamage [] "Tilonalli's Skinshifter"
+        combatDamage ["Bellowing Aegisaur 1"] "Rowdy Crew"
+        combatDamage ["Bellowing Aegisaur 2"] "Needletooth Raptor"
+
+        validateLife Opponent 0
+    ]
+
+
+attributes = attributeFormatter $ do
+  attribute "opponent life" $ countLife Opponent
+  attribute "mana" $
+    (+) <$> countCards
+              (matchAttribute land
+              <> missingAttribute tapped
+              <> matchController Active
+              )
+        <*> countManaPool Active
+
+formatter 1 = attributes <> boardFormatter
+formatter 3 = attributes <>
+  cardFormatter
+    "remaining creatures"
+    (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 4 = attributes <>
+  cardFormatter
+    "non-blocked creatures"
+      (matchLocation (Active, Play)
+      <> matchAttribute attacking
+      <> missingAttribute blocked
+      )
+formatter 5 = attributes <>
+  cardFormatter
+    "damaging creatures"
+    (matchLocation (Active, Play)
+    <> matchAttribute attacking
+    <> (missingAttribute blocked `matchOr` matchAttribute trample)
+    )
+formatter 6 = attributes <>
+  cardFormatter
+    "damaging creatures"
+    (matchLocation (Active, Play)
+    <> matchAttribute attacking
+    <> (missingAttribute blocked `matchOr` matchAttribute trample)
+    )
+formatter _ = attributes
diff --git a/src/Solutions/UltimateMasters.hs b/src/Solutions/UltimateMasters.hs
new file mode 100644
--- /dev/null
+++ b/src/Solutions/UltimateMasters.hs
@@ -0,0 +1,224 @@
+module Solutions.UltimateMasters where
+
+import Control.Lens (over)
+import Control.Monad
+
+import Dovin.V2
+
+sacrificeToAltar mana name = do
+  activate "" "" "Phrexian Altar" >> resolveTop
+  sacrifice name
+  addMana mana
+
+solution :: GameMonad ()
+solution = do
+  step "Initial state" $ do
+    setLife Opponent 20
+
+    withLocation Hand $ do
+      addInstant "Through the Breach"
+      withAttribute arcane $ addInstant "Goryo's Vengeance"
+      addSorcery "Reanimate"
+      addSorcery "Vengeful Rebirth"
+      addCreature (2, 5) "Stingerfling Spider"
+      addCreature (15, 15) "Emrakul, the Aeons Torn"
+
+    withLocation Play $ do
+      addPlaneswalker 3 "Liliana of the Veil"
+      addArtifact "Phrexian Altar"
+      addArtifact "Engineered Explosives"
+      addLands 6 "Swamp"
+      addLands 6 "Mountain"
+
+      withAttribute haste
+        $ withPlusOneCounters 1
+        $ addCreature (4, 3) "Vengevine"
+
+      withAttribute legendary
+        $ withEffect
+            matchInPlay
+            (matchOtherCreatures <> (const $ matchAttributes [creature]))
+            (pure . over cardStrength (mkStrength (1, 1) <>) . setAttribute undying)
+        $ addCreature (5, 5) "Mikaeus, the Unhallowed"
+
+    as Opponent $ do
+      withLocation Play $ do
+        addLands 7 "Plains"
+        addLands 2 "Forest"
+
+        addLand "Dark Depths"
+
+        withAttribute flying $ do
+          addCreature (4, 6) "Reya Dawnbringer"
+          addCreature (4, 3) "Sublime Archangel"
+          withAttribute legendary
+            $ addCreature (5, 5) "Sigarda, Host of Herons"
+
+      withLocation Graveyard $ do
+        addEnchantment "Bridge from Below"
+
+  step "Sac Vengevine and Reanimate with the created mana, exiling Bridge" $ do
+    sacrificeToAltar "B" "Vengevine"
+
+    exile "Bridge from Below"
+
+    cast "B" "Reanimate" >> resolveTop
+    targetInLocation (Active, Graveyard) "Vengevine"
+    returnToPlay "Vengevine"
+
+  step "Sac Vengevine (undying) then Mikaeus for mana" $ do
+    sacrificeToAltar "U" "Vengevine"
+    sacrificeToAltar "U" "Mikaeus, the Unhallowed"
+
+  step "Engineered Explosives for Sigarda" $ do
+    activate "" "2" "Engineered Explosives" >> resolveTop
+    destroy "Sigarda, Host of Herons"
+
+  step "Goryo's Mikaeus with spliced Breach of Stingerfling, destroying Archangel" $ do
+    tapForMana "B" "Swamp 1"
+    tapForMana "B" "Swamp 2"
+    tapForMana "R" "Mountain 1"
+    tapForMana "R" "Mountain 2"
+    tapForMana "R" "Mountain 3"
+    tapForMana "R" "Mountain 4"
+
+    cast "1B" "Goryo's Vengeance"
+    splice "Goryo's Vengeance" "2RR" "Through the Breach"
+    resolveTop
+
+    with "Mikaeus, the Unhallowed" $ \cn -> do
+      targetInLocation (Active, Graveyard) cn
+      validate (matchAttribute legendary) cn
+      returnToPlay cn
+      gainAttribute haste cn
+
+    with "Stingerfling Spider" $ \cn -> do
+      targetInLocation (Active, Hand) cn
+      moveTo Play cn
+      gainAttribute haste cn
+
+      trigger "Destroy creature with flying" cn >> resolveTop
+      target "Sublime Archangel"
+      validate (matchAttribute flying) "Sublime Archangel"
+      destroy "Sublime Archangel"
+
+  step "Liliana to force sac of Reya" $ do
+    activatePlaneswalker 1 "Liliana of the Veil"
+    as Opponent $ do
+      sacrifice "Reya Dawnbringer"
+
+  step "Breach Emrakul" $ do
+    tapForMana "B" "Swamp 3"
+    tapForMana "B" "Swamp 4"
+    tapForMana "B" "Swamp 5"
+    tapForMana "R" "Mountain 5"
+    tapForMana "R" "Mountain 6"
+    cast "4R" "Through the Breach" >> resolveTop
+
+    with "Emrakul, the Aeons Torn" $ \cn -> do
+      targetInLocation (Active, Hand) cn
+      moveTo Play cn
+      gainAttribute haste cn
+
+  step "Attack with everything" $ do
+    attackWith
+      [ "Emrakul, the Aeons Torn"
+      , "Mikaeus, the Unhallowed"
+      , "Vengevine"
+      , "Stingerfling Spider"
+      ]
+
+  step "Assume opponent activates Dark Depths to block Emrakul in response to Annihilator trigger, then annihilates lands" $ do
+    trigger "Annihilator 6" "Emrakul, the Aeons Torn"
+
+    as Opponent $ do
+      forM_ [1..7] $ \n -> tapForMana "W" (numbered n "Plains")
+      forM_ [1..2] $ \n -> tapForMana "G" (numbered n "Forest")
+      activate "" "3" "Dark Depths" >> resolveTop
+      activate "" "3" "Dark Depths" >> resolveTop
+      activate "" "3" "Dark Depths" >> resolveTop
+      sacrifice "Dark Depths"
+      withLocation Play
+        $ withAttributes [indestructible, flying, token]
+        $ addCreature (20, 20) "Marit Large"
+
+    resolve "Annihilator 6"
+    as Opponent $
+      forM_ [1..6] $ \n -> sacrifice (numbered n "Plains")
+
+    gainAttribute "blocked" "Emrakul, the Aeons Torn"
+
+  step "Deal damage. Emrakul returns with undying" $ do
+    forCards
+      (matchLocation (Active, Play) <> matchAttribute attacking <> missingAttribute "blocked")
+      (combatDamage [])
+
+    fight "Emrakul, the Aeons Torn" "Marit Large"
+
+  step "In second main, sacrifice remaining creatures for mana (spider twice)" $ do
+    transitionTo SecondMain
+
+    sacrificeToAltar "R" "Vengevine"
+    sacrificeToAltar "G" "Stingerfling Spider"
+    sacrificeToAltar "U" "Stingerfling Spider" -- From undying
+    sacrificeToAltar "U" "Emrakul, the Aeons Torn"
+    sacrificeToAltar "U" "Mikaeus, the Unhallowed"
+
+  step "Cast Vengeful Rebirth on Mikaeus, targeting opponent" $ do
+    tapForMana "B" "Swamp 6"
+    cast "4GR" "Vengeful Rebirth" >> resolveTop
+
+    targetInLocation (Active, Graveyard) "Mikaeus, the Unhallowed"
+    returnToHand "Mikaeus, the Unhallowed"
+    damage (const 6) (targetPlayer Opponent) "Vengeful Rebirth"
+
+    validateLife 0 Opponent
+
+manaAttribute = attributeFormatter $ attribute "mana" $
+  (+) <$> countCards
+            ( matchAttribute "land"
+            <> missingAttribute "tapped"
+            <> matchController Active
+            )
+      <*> countManaPool Active
+formatter 1 = boardFormatter
+formatter 3 = manaAttribute
+  <> cardFormatter
+       "creatures"
+       (matchLocation (Active, Play) <> matchAttribute creature)
+  <> cardFormatter
+       "graveyard"
+       (matchLocation (Active, Graveyard) <> matchAttribute creature)
+formatter 4 = manaAttribute
+  <> cardFormatter
+       "remaining creatures"
+       (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 5 = manaAttribute
+  <> cardFormatter
+       "remaining creatures"
+       (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 6 = manaAttribute
+  <> cardFormatter
+       "remaining creatures"
+       (matchLocation (Opponent, Play) <> matchAttribute creature)
+formatter 8 =
+  cardFormatter
+    "creatures"
+    (matchLocation (Active, Play) <> matchAttribute creature)
+formatter 9 =
+  cardFormatter
+    "unblocked creatures"
+    (matchLocation (Active, Play)
+    <> matchAttribute creature
+    <> invert (matchAttribute "blocked")
+    )
+formatter 10 =
+     attributeFormatter (attribute "life" (countLife Opponent))
+  <> cardFormatter
+       "creatures"
+       (matchLocation (Active, Play) <> matchAttribute creature)
+formatter 11 = manaAttribute
+  <> attributeFormatter (attribute "life" (countLife Opponent))
+formatter 12 = manaAttribute
+  <> attributeFormatter (attribute "life" (countLife Opponent))
+formatter _ = manaAttribute
diff --git a/test/Activate.hs b/test/Activate.hs
new file mode 100644
--- /dev/null
+++ b/test/Activate.hs
@@ -0,0 +1,25 @@
+module Activate where
+
+import TestPrelude.V2
+
+test_Activate = testGroup "activate"
+  [ prove "adds activated card to stack" $ do
+      withLocation Play $ addArtifact "Dawn of Hope"
+      addMana "3W"
+      activate "Create Soldier" "3W" "Dawn of Hope"
+      validate
+        (matchLocation (Active, Stack) <> matchAttribute activated)
+        "Create Soldier"
+      validateBoardEquals (manaPoolFor Active) mempty
+      resolveTop
+  , refute
+      "requires card in play or graveyard"
+      "in play or graveyard" $ do
+        withLocation Hand $ addArtifact "Dawn of Hope"
+        activate "" "" "Dawn of Hope"
+  , refute
+      "requires card controlled by actor"
+      "has controller Opponent" $ do
+        withLocation Hand $ addArtifact "Dawn of Hope"
+        as Opponent $ activate "" "" "Dawn of Hope"
+  ]
diff --git a/test/Counter.hs b/test/Counter.hs
new file mode 100644
--- /dev/null
+++ b/test/Counter.hs
@@ -0,0 +1,37 @@
+module Counter where
+
+import TestPrelude.V2
+
+test_Case = testGroup "counter"
+  [ prove "removes spell from stack" $ do
+      as Opponent $ do
+        withLocation Hand $ addInstant "Shock"
+        cast "" "Shock"
+        counter "Shock"
+
+        validate
+          (matchLocation (Opponent, Graveyard))
+          "Shock"
+        validateBoardEquals stack mempty
+  , refute
+      "requires card exists"
+      "Card does not exist" $ do
+        counter "Shock"
+  , refute
+      "requires card on stack"
+      "on stack" $ do
+        withLocation Hand $ addInstant "Shock"
+        counter "Shock"
+  , refute
+      "cannot counter trigger"
+      "not has attribute triggered or has attribute activated" $ do
+        withLocation Play $ addArtifact "Dawn of Hope"
+        trigger "Draw Card" "Dawn of Hope"
+        counter "Draw Card"
+  , refute
+      "cannot counter activation"
+      "not has attribute triggered or has attribute activated" $ do
+        withLocation Play $ addArtifact "Dawn of Hope"
+        activate "Create Soldier" "" "Dawn of Hope"
+        counter "Create Soldier"
+  ]
diff --git a/test/Damage.hs b/test/Damage.hs
new file mode 100644
--- /dev/null
+++ b/test/Damage.hs
@@ -0,0 +1,160 @@
+module Damage where
+
+import TestPrelude
+
+test_Damage = testGroup "damage"
+  [ prove "adds damage to a creature" $ do
+      withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+      addInstant "Shock"
+
+      damage (const 2) (targetCard "Angel") "Shock"
+      validate "Angel" $ matchInPlay <> matchDamage 2
+      validateLife Active 0
+      validateLife Opponent 0
+  , prove "removes loyalty counters from a planeswalker" $ do
+      withLocation (Active, Play) $ addPlaneswalker 3 "Jeff"
+      addInstant "Shock"
+      damage (const 2) (targetCard "Jeff") "Shock"
+      validate "Jeff" $ matchInPlay <> matchLoyalty 1
+  , prove "adds damage computed from function" $ do
+      withLocation (Active, Play) $ addCreature (1, 4) "Angel"
+
+      damage ((* 2) . view cardPower) (targetCard "Angel") "Angel"
+      validate "Angel" $ matchDamage 2
+  , prove "does not destroy creature since SBAs aren't run" $ do
+      withLocation (Active, Play) $ addCreature (2, 2) "Angel"
+      addInstant "Shock"
+
+      damage (const 2) (targetCard "Angel") "Shock"
+      validate "Angel" $ matchInPlay <> matchDamage 2
+  , prove "cannot destroy indestructible creatures" $ do
+      withLocation (Active, Play)
+        $ withAttribute indestructible
+        $ addCreature (2, 2) "Angel"
+      addInstant "Shock"
+
+      damage (const 2) (targetCard "Angel") "Shock"
+      validate "Angel" $ matchInPlay <> matchDamage 2
+  , prove "target gains deathtouched when source has deathtouch" $ do
+      withLocation (Active, Play)
+        $ addCreature (2, 2) "Angel"
+      withLocation (Active, Play)
+        $ withAttribute deathtouch
+        $ addCreature (1, 4) "Spider"
+
+      damage (const 1) (targetCard "Angel") "Spider"
+      validate "Angel" $ matchAttribute deathtouched
+  , prove "target does not gain deathtouched when no damage done" $ do
+      withLocation (Active, Play)
+        $ addCreature (2, 2) "Angel"
+      withLocation (Active, Play)
+        $ withAttribute deathtouch
+        $ addCreature (1, 4) "Spider"
+
+      damage (const 0) (targetCard "Angel") "Spider"
+      validate "Angel" $ missingAttribute deathtouched
+  , prove "gains life when source has lifelink" $ do
+      withLocation (Opponent, Play)
+        $ withAttribute lifelink
+        $ addCreature (2, 2) "Angel"
+
+      damage (const 2) (targetCard "Angel") "Angel"
+      validateLife Opponent 2
+  , refute
+      "requires target to be in play"
+      "in play" $ do
+        withLocation (Active, Graveyard) $ addCreature (4, 4) "Angel"
+        addInstant "Shock"
+
+        damage (const 2) (targetCard "Angel") "Shock"
+  , refute
+      "requires target to be a creature"
+      "has attribute creature" $ do
+        withLocation (Active, Play) $ addArtifact "Mox"
+        addInstant "Shock"
+
+        damage (const 2) (targetCard "Mox") "Shock"
+  , refute
+      "requires damage to be >= 0"
+      "damage must be positive, was -1" $ do
+        withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+
+        damage (const (-1)) (targetCard "Angel") "Angel"
+  , prove "damages player" $ do
+      addInstant "Shock"
+      damage (const 2) (targetPlayer Opponent) "Shock"
+
+      validateLife Opponent (-2)
+  ]
+
+test_CombatDamage = testGroup "combatDamage"
+  [ prove "damages opponent when no blockers" $ do
+      withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+      attackWith ["Angel"]
+      combatDamage [] "Angel"
+      validateLife Opponent (-4)
+  , prove "damages blocker instead of player" $ do
+      withLocation (Opponent, Play) $ addCreature (1, 1) "Spirit"
+      withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+      attackWith ["Angel"]
+      combatDamage ["Spirit"] "Angel"
+      validateLife Opponent 0
+      validate "Spirit" $ matchDamage 4
+  , prove "only deals as much damage to blockers as available power" $ do
+      withLocation (Opponent, Play) $ addCreature (1, 1) "Spirit"
+      withLocation (Opponent, Play) $ addCreature (6, 6) "Dragon"
+      withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+      attackWith ["Angel"]
+      combatDamage ["Spirit", "Dragon"] "Angel"
+      validateLife Opponent 0
+      validate "Spirit" $ matchDamage 1
+      validate "Dragon" $ matchDamage 3
+      validate "Angel" $ matchDamage 7
+  , prove "deals excess damage to player with trample" $ do
+      withLocation (Opponent, Play) $ addCreature (1, 1) "Spirit"
+      withLocation (Active, Play)
+        $ withAttributes [lifelink, trample]
+        $ addCreature (4, 4) "Angel"
+      attackWith ["Angel"]
+      combatDamage ["Spirit"] "Angel"
+      validateLife Opponent (-3)
+      validateLife Active 4
+  , prove "deals all damage, primarily for lifelink purposes" $ do
+      withLocation (Opponent, Play) $ addCreature (1, 1) "Spirit"
+      withLocation (Active, Play)
+        $ withAttributes [lifelink]
+        $ addCreature (4, 4) "Angel"
+      attackWith ["Angel"]
+      combatDamage ["Spirit"] "Angel"
+      validateLife Active 4
+  , prove "deals damage to opposing player of actor" $ do
+      as Opponent $ do
+        withLocation (Opponent, Play) $ addCreature (4, 4) "Angel"
+        attackWith ["Angel"]
+        combatDamage [] "Angel"
+        validateLife Active (-4)
+  , refute
+      "requires attacking creature"
+      "has attribute attacking" $ do
+        withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+        combatDamage [] "Angel"
+  , refute
+      "requires in play creature"
+      "in play" $ do
+        withLocation (Active, Graveyard) $ addCreature (4, 4) "Angel"
+        gainAttribute attacking "Angel"
+        combatDamage [] "Angel"
+  , refute
+      "requires in play blocker"
+      "in play" $ do
+        withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+        withLocation (Opponent, Graveyard) $ addCreature (1, 1) "Spirit"
+        gainAttribute attacking "Angel"
+        combatDamage ["Spirit"] "Angel"
+  , refute
+      "requires control of attacking creature"
+      "has controller Opponent" $ do
+        withLocation (Active, Play) $ addCreature (4, 4) "Angel"
+        attackWith ["Angel"]
+        as Opponent $ combatDamage [] "Angel"
+  ]
diff --git a/test/Discard.hs b/test/Discard.hs
new file mode 100644
--- /dev/null
+++ b/test/Discard.hs
@@ -0,0 +1,18 @@
+module Discard where
+
+import TestPrelude.V2
+
+test_Cases = testGroup "jumpstart"
+  [ prove "discards card from hand to graveyard" $ do
+      as Opponent $ do
+        withLocation Hand $ addLand "Mountain"
+        discard "Mountain"
+        validate
+          (matchLocation (Opponent, Graveyard))
+          "Mountain"
+  , refute
+      "requires card in hand"
+      "in location (Active,Hand)" $ do
+        withLocation Play $ addLand "Mountain"
+        discard "Mountain"
+  ]
diff --git a/test/Driver.hs b/test/Driver.hs
new file mode 100644
--- /dev/null
+++ b/test/Driver.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}
diff --git a/test/Exert.hs b/test/Exert.hs
new file mode 100644
--- /dev/null
+++ b/test/Exert.hs
@@ -0,0 +1,16 @@
+module Exert where
+
+import TestPrelude
+
+test_Move = testGroup "exert"
+  [ prove "exerts an attacking creature" $ do
+      withLocation (Active, Play) $ addCreature (1, 1) "Bat"
+      tap "Bat"
+      exert "Bat"
+      validate "Bat" $ matchAttribute exerted
+  , refute
+      "requires tapped creature"
+      "has attribute tapped" $ do
+        withLocation (Active, Play) $ addCreature (1, 1) "Bat"
+        exert "Bat"
+  ]
diff --git a/test/Flashback.hs b/test/Flashback.hs
new file mode 100644
--- /dev/null
+++ b/test/Flashback.hs
@@ -0,0 +1,20 @@
+module Flashback where
+
+import TestPrelude.V2
+
+test_Flashback = testGroup "flashback"
+  [ prove "casts from graveyard to stack" $ do
+      as Opponent $ do
+        withLocation Graveyard $ addInstant "Shock"
+        addMana "R"
+        flashback "R" "Shock"
+        validate
+          (matchLocation (Opponent, Stack) <> matchAttribute exileWhenLeaveStack)
+          "Shock"
+        validateBoardEquals (manaPoolFor Active) mempty
+  , refute
+      "requires card in graveyard"
+      "in location (Active,Graveyard)" $ do
+        withLocation Hand $ addInstant "Shock"
+        flashback "" "Shock"
+  ]
diff --git a/test/Jumpstart.hs b/test/Jumpstart.hs
new file mode 100644
--- /dev/null
+++ b/test/Jumpstart.hs
@@ -0,0 +1,31 @@
+module Jumpstart where
+
+import TestPrelude.V2
+
+test_Cases = testGroup "jumpstart"
+  [ prove "casts from graveyard to stack" $ do
+      as Opponent $ do
+        withLocation Graveyard $ addInstant "Shock"
+        withLocation Hand $ addLand "Mountain"
+        addMana "R"
+        jumpstart "R" "Mountain" "Shock"
+        validate
+          (matchLocation (Opponent, Stack) <> matchAttribute exileWhenLeaveStack)
+          "Shock"
+        validate
+          (matchLocation (Opponent, Graveyard))
+          "Mountain"
+        validateBoardEquals (manaPoolFor Active) mempty
+  , refute
+      "requires card in graveyard"
+      "in location (Active,Graveyard)" $ do
+        withLocation Hand $ addInstant "Shock"
+        withLocation Hand $ addLand "Mountain"
+        jumpstart "" "Mountain" "Shock"
+  , refute
+      "requires discard card in hand"
+      "in location (Active,Hand)" $ do
+        withLocation Hand $ addInstant "Shock"
+        withLocation Play $ addLand "Mountain"
+        jumpstart "" "Mountain" "Shock"
+  ]
diff --git a/test/Move.hs b/test/Move.hs
new file mode 100644
--- /dev/null
+++ b/test/Move.hs
@@ -0,0 +1,103 @@
+module Move where
+
+import TestPrelude
+
+test_Move = testGroup "move/moveTo"
+  [ prove "moves card from one location to another" $ do
+      withLocation (Active, Hand) $ addLand "Forest"
+      move (Active, Hand) (Active, Exile) "Forest"
+
+      validate "Forest" $ matchLocation (Active, Exile)
+  , prove "exiles jumpstart'ed cards" $ do
+      withLocation (Active, Stack) $ addInstant "Chemister's Insight"
+      gainAttribute exileWhenLeaveStack "Chemister's Insight"
+
+      move (Active, Stack) (Active, Graveyard) "Chemister's Insight"
+
+      validate "Chemister's Insight" $
+           matchLocation (Active, Exile)
+        <> missingAttribute exileWhenLeaveStack
+  , prove "adds summoned attribute when moving to play" $ do
+      withLocation (Active, Hand) $ addLand "Forest"
+      move (Active, Hand) (Active, Play) "Forest"
+
+      validate "Forest" $ matchAttribute summoned
+  , prove "removes gained attribute when leaving play" $ do
+      withLocation (Active, Play) $ addLand "Forest"
+
+      gainAttribute "bogus" "Forest"
+
+      move (Active, Play) (Active, Hand) "Forest"
+
+      validate "Forest" $ missingAttribute "bogus"
+  , prove "adds +1/+1 to when undying" $ do
+      withLocation (Active, Play)
+        $ withAttribute undying
+        $ addCreature (1, 1) "Zombie"
+
+      moveTo Graveyard "Zombie"
+
+      validate "Zombie" $
+        matchLocation (Active, Play) <> matchPlusOneCounters 1
+  , prove "moves to graveyard when undying and has +1/+1 counters" $ do
+      withLocation (Active, Play)
+        $ withAttribute undying
+        $ withPlusOneCounters 3
+        $ addCreature (1, 1) "Zombie"
+
+      moveTo Graveyard "Zombie"
+
+      validate "Zombie" $
+        matchLocation (Active, Graveyard) <> matchPlusOneCounters 0
+  , prove "removes damage when leaving play" $ do
+      withLocation (Active, Play) $ addCreature (1, 1) "Zombie"
+      modifyCard "Zombie" cardDamage (const 1)
+
+      moveTo Graveyard "Zombie"
+
+      validate "Zombie" $ matchDamage 0
+  , prove "moves card to graveyard of same owner" $ do
+      withLocation (Opponent, Hand) $ addLand "Forest"
+      moveTo Graveyard "Forest"
+      validate "Forest" $ matchLocation (Opponent, Graveyard)
+  , prove "can change controller of token" $ do
+      withLocation (Active, Play)
+        $ withAttribute token
+        $ addArtifact "Treasure"
+
+      move (Active, Play) (Opponent, Play) "Treasure"
+      validate "Treasure" $ matchLocation (Opponent, Play)
+  , refute
+      "cannot move to stack"
+      "cannot move directly to stack" $ do
+        withLocation (Active, Hand) $ addInstant "Shock"
+
+        move (Active, Hand) (Active, Stack) "Shock"
+  , refute
+      "requires card exists"
+      "Card does not exist: Forest" $ do
+        move (Active, Hand) (Active, Exile) "Forest"
+  , refute
+      "cannot move to same location"
+      "cannot move to same location" $ do
+        withLocation (Active, Hand) $ addInstant "Shock"
+
+        move (Active, Hand) (Active, Hand) "Shock"
+  , refute
+      "cannot move token from non-play location"
+      "cannot move token from non-play location" $ do
+        withLocation (Active, Graveyard)
+          $ withAttribute token
+          $ addArtifact "Treasure"
+
+        move (Active, Graveyard) (Active, Play) "Treasure"
+  , refute
+      "cannot move copy from non-stack location"
+      "cannot move copy from non-stack location" $ do
+        withLocation (Active, Hand) $ addInstant "Shock"
+
+        cast "" "Shock"
+        copySpell "Shock" "Shock 1" >> resolveTop
+
+        move (Active, Graveyard) (Active, Play) "Shock 1"
+  ]
diff --git a/test/Resolve.hs b/test/Resolve.hs
new file mode 100644
--- /dev/null
+++ b/test/Resolve.hs
@@ -0,0 +1,58 @@
+module Resolve where
+
+import TestPrelude.V2
+
+test_Resolve = testGroup "resolve"
+  [ testGroup "resolveTop"
+    [ prove "resolves top spell from stack" $ do
+        withLocation Hand $ addInstant "Shock"
+        cast "" "Shock" >> resolveTop
+
+        validate (matchLocation (Active, Graveyard)) "Shock"
+        validateBoardEquals stack mempty
+    , prove "resolves top permanent of stack" $ do
+        withLocation Hand $ addArtifact "Mox Opal"
+        cast "" "Mox Opal" >> resolveTop
+
+        validate (matchLocation (Active, Play)) "Mox Opal"
+        validateBoardEquals stack mempty
+    , prove "resolves top trigger of stack" $ do
+        withLocation Play $ addArtifact "Phrexian Altar"
+        trigger "Trigger" "Phrexian Altar" >> resolveTop
+
+        validateBoardEquals stack mempty
+        validateRemoved "Trigger"
+    , prove "resolves top activation of stack" $ do
+        withLocation Play $ addArtifact "Phrexian Altar"
+        activate "Mana Ability" "" "Phrexian Altar" >> resolveTop
+
+        validateBoardEquals stack mempty
+        validateRemoved "Mana Ability"
+    , refute
+        "requires non-empty stack"
+        "stack is empty" $ do
+          resolveTop
+    ]
+  , testGroup "resolve"
+    [ prove "resolves top card of stack" $ do
+        withLocation Hand $ addInstant "Shock"
+        cast "" "Shock" >> resolve "Shock"
+
+        validate (matchLocation (Active, Graveyard)) "Shock"
+        validateBoardEquals stack mempty
+    , refute
+        "requires top card to match provided"
+        "unexpected top of stack: expected Shock 1, got Shock 2" $ do
+          withLocation Hand $ addInstant "Shock 1"
+          withLocation Hand $ addInstant "Shock 2"
+          cast "" "Shock 1"
+          cast "" "Shock 2"
+          resolve "Shock 1"
+    , refute
+        "requires non-empty stack"
+        "stack is empty" $ do
+          withLocation Hand $ addInstant "Shock"
+          resolve "Shock"
+    ]
+  ]
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,291 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Spec where
+
+import TestPrelude
+
+test_Test = testGroup "Actions"
+  [ testGroup "cast"
+    [ prove "casts from hand to stack" $ do
+        withLocation (Active, Hand) $ addCreature (1, 1) "Zombie"
+        addMana "B"
+        castFromLocation (Active, Hand) "B" "Zombie"
+        validate "Zombie" $ matchLocation (Active, Stack)
+        validateBoardEquals (manaPoolFor Active) mempty
+    , prove "can cast as opponent" $ do
+        as Opponent $ do
+          withLocation (Opponent, Hand) $ addCreature (1, 1) "Zombie"
+          addMana "B"
+          castFromLocation (Opponent, Hand) "B" "Zombie"
+          validate "Zombie" $ matchLocation (Opponent, Stack)
+          validateBoardEquals (manaPoolFor Opponent) mempty
+    , refute
+        "requires card to be in hand"
+        "Zombie does not match requirements: in location (Active,Hand)" $ do
+          withLocation (Active, Play) $ addCreature (1, 1) "Zombie"
+          cast "" "Zombie"
+    ]
+  , testGroup "castFromLocation"
+    [ prove "places card on top of stack, spending mana" $ do
+        withLocation (Active, Graveyard) $ addCreature (1, 1) "Zombie"
+        addMana "B"
+        castFromLocation (Active, Graveyard) "B" "Zombie"
+        validate "Zombie" $ matchLocation (Active, Stack)
+        validateBoardEquals (manaPoolFor Active) mempty
+
+    , refute
+        "requires mana be available"
+        "Mana pool () does not contain (B)" $ do
+          withLocation (Active, Hand) $ addCreature (1, 1) "Zombie"
+          castFromLocation (Active, Hand) "B" "Zombie"
+
+    , prove "can cast non-instant in second main" $ do
+        withLocation (Active, Hand) $ addSorcery "Lava Spike"
+        transitionTo SecondMain
+        castFromLocation (Active, Hand) "" "Lava Spike"
+
+    , refute
+        "requires main phase for non-instant"
+        "not in a main phase" $ do
+          withLocation (Active, Hand) $ addSorcery "Lava Spike"
+          transitionTo BeginCombat
+          castFromLocation (Active, Hand) "" "Lava Spike"
+
+    , refute
+        "requires stack to be empty for non-instant"
+        "stack is not empty" $ do
+          withLocation (Active, Hand) $ addInstant "Shock"
+          withLocation (Active, Hand) $ addSorcery "Lava Spike"
+
+          castFromLocation (Active, Hand) "" "Shock"
+          castFromLocation (Active, Hand) "" "Lava Spike"
+
+    , prove "increases storm count if instant" $ do
+        withLocation (Active, Hand) $ addInstant "Shock"
+        castFromLocation (Active, Hand) "" "Shock"
+        validateBoardEquals (counters . at "storm" . non 0) 1
+
+    , prove "increases storm count if sorcery" $ do
+        withLocation (Active, Hand) $ addSorcery "Lava Spike"
+        castFromLocation (Active, Hand) "" "Lava Spike"
+
+    , prove "does not increase storm count otherwise" $ do
+        withLocation (Active, Hand) $ addArtifact "Mox Amber"
+        castFromLocation (Active, Hand) "" "Mox Amber"
+        validateBoardEquals (counters . at "storm" . non 0) 0
+    ]
+  , testGroup "spendMana"
+    [ prove "removes colored mana from pool" $ do
+        addMana "BBRRRWW"
+        spendMana "RB"
+        validateBoardEquals (manaPoolFor Active) "BRRWW"
+    , prove "removes colorless mana from pool" $ do
+        addMana "RWB"
+        spendMana "3"
+        validateBoardEquals (manaPoolFor Active) mempty
+    , prove "removes multiple digits for colorless mana from pool" $ do
+        addMana "9"
+        addMana "9"
+        spendMana "15"
+        validateBoardEquals (manaPoolFor Active) "XXX"
+    , prove "removes colored mana before colorless" $ do
+        addMana "RWB"
+        spendMana "1R"
+        validateBoardEquals (manaPoolFor Active) "W"
+    , refute
+        "requires sufficient mana (colorless)"
+        "Mana pool () does not contain (X)" $ do
+          spendMana "1"
+    , refute
+        "requires sufficient mana (colored)"
+        "Mana pool () does not contain (X)" $ do
+          addMana "R"
+          spendMana "2"
+    , refute
+        "requires right color mana"
+        "Mana pool (R) does not contain (W)" $ do
+          addMana "R"
+          spendMana "W"
+    ]
+  , testGroup "addMana"
+    [ prove "adds mana to pool" $ do
+        addMana "2RG"
+        validateBoardEquals (manaPool . at Active . _Just) "GRXX"
+    , prove "adds mana with multiple digits to pool" $ do
+        addMana "10"
+        validateBoardEquals (manaPool . at Active . _Just) (replicate 10 'X')
+    ]
+  , testGroup "tap"
+    [ prove "taps card in play" $ do
+        withLocation (Active, Play) $ addLand "Forest"
+        tap "Forest"
+
+        validate "Forest" $ matchAttribute tapped
+    , prove "taps card in opponent's play" $ do
+        withLocation (Active, Play) $ addLand "Forest"
+        tap "Forest"
+
+        validate "Forest" $ matchAttribute tapped
+    , refute
+        "requires card exists"
+        "Card does not exist: Forest" $ do
+          tap "Forest"
+    , refute
+        "requires untapped"
+        "not has attribute tapped" $ do
+          withAttribute tapped $ withLocation (Active, Play) $ addLand "Forest"
+          tap "Forest"
+    , refute
+        "requires in play"
+        "in play" $ do
+          withLocation (Active, Graveyard) $ addLand "Forest"
+          tap "Forest"
+    ]
+  , testGroup "tapForMana"
+    [ prove "taps card and adds mana to pool" $ do
+        withLocation (Active, Play) $ addLand "Forest"
+        tapForMana "G" "Forest"
+
+        validate "Forest" $ matchAttribute tapped
+        validateBoardEquals (manaPoolFor Active) "G"
+    ]
+  , testGroup "transitionTo"
+    [ prove "moves to new state" $ do
+        transitionTo BeginCombat
+        validatePhase BeginCombat
+    , prove "empties mana pool" $ do
+        addMana "B"
+        transitionTo BeginCombat
+        validateBoardEquals manaPool mempty
+    , refute
+        "requires later phase"
+        "FirstMain does not occur after BeginCombat" $ do
+          transitionTo BeginCombat
+          transitionTo FirstMain
+    ]
+  , testGroup "transitionToForced"
+    [ prove "can transition backwards" $ do
+        transitionTo BeginCombat
+        transitionToForced FirstMain
+        validatePhase FirstMain
+    ]
+  , testGroup "untap"
+    [ prove "untaps card in play" $ do
+        withLocation (Active, Play) $ withAttribute tapped $  addLand "Forest"
+        untap "Forest"
+
+        validate "Forest" $ missingAttribute tapped
+    , prove "untaps card in opponent's play" $ do
+        withLocation (Opponent, Play) $ withAttribute tapped $ addLand "Forest"
+        untap "Forest"
+
+        validate "Forest" $ missingAttribute tapped
+    , refute
+        "requires card exists"
+        "Card does not exist: Forest" $ do
+          untap "Forest"
+    , refute
+        "requires tapped"
+        "has attribute tapped" $ do
+          withLocation (Active, Play) $ addLand "Forest"
+          untap "Forest"
+    , refute
+        "requires in play"
+        "in play" $ do
+          withLocation (Active, Graveyard) $ addLand "Forest"
+          untap "Forest"
+    ]
+  , testGroup "splice"
+    [ prove "splices on to an arcane spell" $ do
+        withLocation (Active, Hand) $ do
+          addInstant "Glacial Ray"
+          withAttribute arcane $ addInstant "Lava Spike"
+
+        addMana "RRR"
+        cast "R" "Lava Spike"
+        splice "Lava Spike" "1R" "Glacial Ray"
+        resolveTop
+
+        validate "Glacial Ray" $ matchLocation (Active, Hand)
+        validateBoardEquals stack mempty
+        validateBoardEquals (manaPoolFor Active) mempty
+    , prove "can splice as opponent" $ do
+        withLocation (Opponent, Hand) $ do
+          addInstant "Glacial Ray"
+          withAttribute arcane $ addInstant "Lava Spike"
+
+        as Opponent $ do
+          addMana "RRR"
+          cast "R" "Lava Spike"
+          splice "Lava Spike" "1R" "Glacial Ray"
+          resolveTop
+
+          validate "Glacial Ray" $ matchLocation (Opponent, Hand)
+          validateBoardEquals stack mempty
+          validateBoardEquals (manaPoolFor Opponent) mempty
+    , refute
+      "requires arcane"
+      "has attribute arcane" $ do
+        withLocation (Active, Hand) $ do
+          addInstant "Glacial Ray"
+          addInstant "Lava Spike"
+
+        cast "" "Lava Spike"
+        splice "Lava Spike" "" "Glacial Ray"
+    , refute
+      "requires spliced spell on stack"
+      "Lava Spike not on stack" $ do
+        withLocation (Active, Hand) $ do
+          addInstant "Glacial Ray"
+          withAttribute arcane $ addInstant "Lava Spike"
+
+        splice "Lava Spike" "" "Glacial Ray"
+    , refute
+      "requires spell in hand"
+      "Glacial Ray not in hand" $ do
+        withLocation (Active, Graveyard) $
+          addInstant "Glacial Ray"
+        withLocation (Active, Hand) $
+          withAttribute arcane $ addInstant "Lava Spike"
+
+        cast "" "Lava Spike"
+        splice "Lava Spike" "" "Glacial Ray"
+    ]
+  , testGroup "attackWith"
+    [ prove "attacks with listed creatures" $ do
+        withLocation (Active, Play) $ do
+          addCreature (1, 1) "Bat 1"
+          addCreature (1, 1) "Bat 2"
+          addCreature (1, 1) "Bat 3"
+
+        attackWith ["Bat 1", "Bat 2"]
+
+        validatePhase DeclareAttackers
+        validate "Bat 1" $ matchAttributes [attacking, tapped]
+        validate "Bat 2" $ matchAttributes [attacking, tapped]
+        validate "Bat 3" $ missingAttribute attacking
+        validate "Bat 3" $ missingAttribute tapped
+    , prove "does not tap vigilant attackers" $ do
+        withLocation (Active, Play) $ do
+          withAttribute vigilance $ addCreature (1, 1) "Bat"
+
+        attackWith ["Bat"]
+        validate "Bat" $ matchAttribute attacking
+        validate "Bat" $ missingAttribute tapped
+    , refute
+        "prevents summoned creatures from attacking"
+        "does not have summoning sickness" $ do
+          withLocation (Active, Play) $ do
+            withAttributes [summoned] $ addCreature (1, 1) "Bat"
+
+          attackWith ["Bat"]
+    , prove "allows hasty creatures to attack" $ do
+        withLocation (Active, Play) $ do
+          withAttributes [haste, summoned] $ addCreature (1, 1) "Bat"
+
+        attackWith ["Bat"]
+        validate "Bat" $ matchAttributes [attacking, tapped]
+    ]
+  ]
+
diff --git a/test/StateBasedActions.hs b/test/StateBasedActions.hs
new file mode 100644
--- /dev/null
+++ b/test/StateBasedActions.hs
@@ -0,0 +1,60 @@
+module StateBasedActions where
+
+import TestPrelude
+
+test_SBAs = testGroup "state-based actions"
+  [ prove "destroys creature with damage exceeding toughness" $ do
+      withStateBasedActions $ do
+        withLocation (Active, Play)
+          $ addCreature (1, 1) "Spirit"
+
+        damage (const 2) (targetCard "Spirit") "Spirit"
+
+      validate "Spirit" $ matchLocation (Active, Graveyard)
+  , prove "destroys deathtouched creature" $ do
+      withStateBasedActions $ do
+        withLocation (Active, Play)
+          $ withAttribute deathtouched
+          $ addCreature (1, 1) "Spirit"
+
+      validate "Spirit" $ matchLocation (Active, Graveyard)
+  , prove "does not destroy indestructible creature" $ do
+      withStateBasedActions $ do
+        withLocation (Active, Play)
+          $ withAttributes [indestructible, deathtouched]
+          $ addCreature (1, 1) "Spirit"
+
+        damage (const 2) (targetCard "Spirit") "Spirit"
+
+      validate "Spirit" $ matchInPlay
+   , prove "removes tokens not in play" $ do
+       withStateBasedActions $ do
+         withLocation (Active, Graveyard)
+           $ withAttribute token
+           $ addArtifact "Treasure"
+
+       validateRemoved "Treasure"
+   , prove "does not remove copies on stack" $ do
+       withStateBasedActions $ do
+         withLocation (Active, Hand)
+           $ withAttribute copy
+           $ addArtifact "Shock"
+         cast "" "Shock"
+
+       validate "Shock" $ matchLocation (Active, Stack)
+   , prove "removes copies not on stack" $ do
+       withStateBasedActions $ do
+         withLocation (Active, Graveyard)
+           $ withAttribute copy
+           $ addArtifact "Shock"
+
+       validateRemoved "Shock"
+   , prove "correctly removes damaged tokens" $ do
+       withStateBasedActions $ do
+         withLocation (Active, Play)
+           $ withAttribute token
+           $ addCreature (1, 1) "Spirit"
+
+         damage (const 1) (targetCard "Spirit") "Spirit"
+       validateRemoved "Spirit"
+  ]
diff --git a/test/TestPrelude.hs b/test/TestPrelude.hs
new file mode 100644
--- /dev/null
+++ b/test/TestPrelude.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module TestPrelude
+  ( module Test.Tasty
+  , module Test.Tasty.HUnit
+  , module Dovin.V1
+  , module Control.Lens
+  , module Control.Monad
+  , prove
+  , refute
+  , validateBoardEquals
+  ) where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Dovin.V1
+import Dovin.Monad
+
+import Data.List (isInfixOf)
+
+import Control.Monad
+import Control.Lens
+import Control.Monad.Except
+
+
+prove name m = testCase name $
+  case runMonad emptyBoard m of
+    (Left msg, _, _) -> assertFailure msg
+    (Right (), _, _) -> return mempty
+
+refute name expectedFailure m = testCase name $
+  case runMonad emptyBoard m of
+    (Left msg, _, _) -> assertBool ("expected: " <> expectedFailure <> "\n but got: " <> msg) $ expectedFailure `isInfixOf` msg
+    (Right (), _, _) -> assertFailure "proof was not refuted"
+
+validateBoardEquals lens expected = do
+  x <- use lens
+
+  unless (x == expected) $
+    throwError ("want: " <> show expected <> ", got: " <> show x)
+
diff --git a/test/TestPrelude/V2.hs b/test/TestPrelude/V2.hs
new file mode 100644
--- /dev/null
+++ b/test/TestPrelude/V2.hs
@@ -0,0 +1,13 @@
+module TestPrelude.V2
+  ( module TestPrelude
+  , module Dovin.V2
+  ) where
+
+import Dovin.V2
+import TestPrelude hiding
+  ( activate
+  , trigger
+  , validate
+  , validateLife
+  , withLocation
+  )
diff --git a/test/TestSolutions.hs b/test/TestSolutions.hs
new file mode 100644
--- /dev/null
+++ b/test/TestSolutions.hs
@@ -0,0 +1,10 @@
+module TestSolutions where
+
+import TestPrelude
+
+import qualified Solutions
+
+test_Solutions = testGroup "Solutions" $
+  map solutionTestCase Solutions.all
+
+solutionTestCase (name, solution, _) = prove name solution
diff --git a/test/Trigger.hs b/test/Trigger.hs
new file mode 100644
--- /dev/null
+++ b/test/Trigger.hs
@@ -0,0 +1,23 @@
+module Trigger where
+
+import TestPrelude.V2
+
+test_Trigger = testGroup "trigger"
+  [ prove "adds triggered card to stack" $ do
+      withLocation Play $ addArtifact "Dawn of Hope"
+      trigger "Draw Card" "Dawn of Hope"
+      validate
+        (matchLocation (Active, Stack) <> matchAttribute triggered)
+        "Draw Card"
+      resolveTop
+  , refute
+      "requires card in play or graveyard"
+      "in play or graveyard" $ do
+        withLocation Hand $ addArtifact "Dawn of Hope"
+        trigger "" "Dawn of Hope"
+  , refute
+      "requires card controlled by actor"
+      "has controller Opponent" $ do
+        withLocation Hand $ addArtifact "Dawn of Hope"
+        as Opponent $ trigger "" "Dawn of Hope"
+  ]