From 1fc9dba3b65086e65771bc69af5aea67332e03b9 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Thu, 20 Jun 2024 16:45:34 -0400
Subject: [PATCH 01/16] Make obligation checking more configurable

---
 crucible-cli/src/Lang/Crucible/CLI.hs         |  12 +-
 crucible-symio/tests/TestMain.hs              |   4 +-
 .../src/Lang/Crucible/Syntax/Overrides.hs     |  27 +-
 crucible/src/Lang/Crucible/Backend/Prove.hs   | 361 ++++++++++++++----
 4 files changed, 306 insertions(+), 98 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index 744ea359d..137c4fe4d 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -49,7 +49,7 @@ import Lang.Crucible.Syntax.SExpr
 
 import Lang.Crucible.Analysis.Postdom
 import Lang.Crucible.Backend
-import Lang.Crucible.Backend.Prove (ProofResult(..), proveCurrentObligations)
+import qualified Lang.Crucible.Backend.Prove as Prove
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
@@ -181,12 +181,14 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        getProofObligations bak >>= \case
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
                          Just {} -> hPutStrLn outh "==== Proof obligations ===="
-                       proveCurrentObligations bak defaultLogData z3Adapter $ \goal res -> do
+                       let prover = Prove.offlineProver sym defaultLogData z3Adapter
+                       let strat = Prove.ProofStrategy prover Prove.keepGoing
+                       Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
                          hPrint outh =<< ppProofObligation sym goal
                          case res of
-                           Proved {} -> hPutStrLn outh "PROVED"
-                           Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
-                           Unknown {} -> hPutStrLn outh "UNKNOWN"
+                           Prove.Proved {} -> hPutStrLn outh "PROVED"
+                           Prove.Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
+                           Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
 
                   _ -> hPutStrLn outh "No suitable main function found"
 
diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs
index 24fc89b6a..e390a7b5e 100644
--- a/crucible-symio/tests/TestMain.hs
+++ b/crucible-symio/tests/TestMain.hs
@@ -134,7 +134,9 @@ runFSTest' bak (FSTest fsTest) = do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
 
-  CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation ->
+  let prover = CB.offlineProver sym WSA.defaultLogData W4Y.yicesAdapter
+  let strat = CB.ProofStrategy prover CB.failFast
+  CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
     \case
       CB.Proved {} -> return ()
       CB.Unknown {} -> T.assertFailure "Inconclusive"
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index 8e69a1628..1f749e011 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -10,20 +10,18 @@ module Lang.Crucible.Syntax.Overrides
   ) where
 
 import Control.Lens hiding ((:>), Empty)
-import Control.Monad (forM_)
 import Control.Monad.IO.Class
 import System.IO
 
 import Data.Parameterized.Context hiding (view)
 
 import What4.Expr.Builder
-import What4.Interface
 import What4.ProgramLoc
-import What4.SatResult
 import What4.Solver (LogData(..), defaultLogData)
-import What4.Solver.Z3 (runZ3InOverride)
+import What4.Solver.Z3 (z3Adapter)
 
 import Lang.Crucible.Backend
+import qualified Lang.Crucible.Backend.Prove as CB
 import Lang.Crucible.Types
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
@@ -48,15 +46,14 @@ proveObligations =
      liftIO $ do
        hPutStrLn h "Attempting to prove all outstanding obligations!\n"
 
-       obls <- maybe [] goalsToList <$> getProofObligations bak
-       clearProofObligations bak
+       let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
+                                    , logReason = "assertion proof" }
+       let prover = CB.offlineProver sym logData z3Adapter
+       let strat = CB.ProofStrategy prover CB.keepGoing
+       CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
+         \case
+           CB.Proved {}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+           CB.Disproved {} -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+           CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
 
-       forM_ obls $ \o ->
-         do asms <- assumptionsPred sym (proofAssumptions o)
-            gl <- notPred sym (o ^. to proofGoal.labeledPred)
-            let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
-                                         , logReason = "assertion proof" }
-            runZ3InOverride sym logData [asms,gl] $ \case
-              Unsat{}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-              Sat _mdl -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-              Unknown  -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       clearProofObligations bak
diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 01c14e85b..2d6196658 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -3,32 +3,122 @@ Module      : Lang.Crucible.Backend.Prove
 Description : Proving goals under assumptions
 Copyright   : (c) Galois, Inc 2024
 License     : BSD3
+
+This module contains helpers to dispatch the proof obligations arising from
+symbolic execution using SMT solvers. There are several dimensions of
+configurability, encapsulated in a 'ProofStrategy':
+
+* Offline vs. online: Offline solvers ('offlineProver') are simpler to manage
+  and more easily parallelized, but starting processes adds overhead, and online
+  solvers ('onlineProver') can share state as assumptions are added. See the
+  top-level README for What4 for further discussion of this choice.
+* Failing fast ('failFast') vs. keeping going ('keepGoing')
+* Parallelism and timeouts: Not yet available via helpers in this module, but
+  may be added to a 'ProofStrategy' by clients.
+
+Once an appropriate strategy has been selected, it can be passed to entrypoints
+such as 'proveObligations' to dispatch proof obligations.
+
+When proving a single goal, the overall approach is:
+
+* Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
+  from branch conditions).
+* Negate the goal ('CB.Assertion') that we are trying to prove.
+* Attempt to prove the conjunction of the assumptions and the negated goal.
+
+If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample
+that makes the original goal false, so we have disproven the goal. If the
+negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the
+original goal is proven.
+
+Another way to think of this is as the negated material conditional
+(implication) @not (assumptions -> assertion)@. This formula is equivalent
+to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not
+assertion)@.
 -}
 
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Lang.Crucible.Backend.Prove
-  ( ProofResult(..)
-  , proveGoal
-  , proveProofGoal
+  ( -- * Strategy
+    ProofResult(..)
+  , ProofConsumer(..)
+  , ProofStrategy(..)
+    -- ** Combiner
+  , SubgoalResult(..)
+  , Combiner(..)
+  , keepGoing
+  , failFast
+    -- ** Prover
+  , Prover(..)
+    -- *** Offline
+  , offlineProve
+  , offlineProver
+    -- *** Online
+  , onlineProve
+  , onlineProver
+    -- * Proving goals
   , proveGoals
   , proveObligations
   , proveCurrentObligations
   ) where
 
 import           Control.Lens ((^.))
-import           Data.Functor.Const (Const(Const, getConst))
+import           Control.Monad.Catch (MonadMask)
+import           Control.Monad.IO.Class (MonadIO(liftIO))
+import qualified Control.Monad.Reader as Reader
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
-import qualified What4.Solver.Adapter as WSA
+import qualified What4.Protocol.Online as WPO
+import qualified What4.Protocol.SMTWriter as W4SMT
 import qualified What4.SatResult as W4R
+import qualified What4.Solver.Adapter as WSA
 
 import qualified Lang.Crucible.Backend as CB
 import           Lang.Crucible.Backend.Assumptions (Assumptions)
-import           Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions)
+
+-- | Local helper
+consumeGoals ::
+  -- | Consume an 'Assuming'
+  (asmp -> a -> a) ->
+  -- | Consume a 'Prove'
+  (goal -> a) ->
+  -- | Consume a 'ProveConj'
+  (a -> a -> a) ->
+  CB.Goals asmp goal ->
+  a
+consumeGoals onAssumption onGoal onConj = go
+  where
+  go (CB.Prove gl) = onGoal gl
+  go (CB.Assuming as gl) = onAssumption as (go gl)
+  go (CB.ProveConj g1 g2) = onConj (go g1) (go g2)
+
+-- | Local helper
+consumeGoalsWithAssumptions ::
+  Monoid asmp =>
+  -- | Consume a 'Prove'
+  (asmp -> goal -> a) ->
+  -- | Consume a 'ProveConj'
+  (a -> a -> a) ->
+  CB.Goals asmp goal ->
+  a
+consumeGoalsWithAssumptions onGoal onConj goals =
+  Reader.runReader (go goals) mempty
+  where
+  go =
+    consumeGoals
+      (\asmp gl -> Reader.local (<> asmp) gl)
+      (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
+      (\g1 g2 -> onConj <$> g1 <*> g2)
+
+---------------------------------------------------------------------
+-- * Strategy
 
 -- | The result of attempting to prove a goal with an SMT solver.
 --
@@ -40,6 +130,9 @@ data ProofResult sym t
      Proved
      -- | The goal was disproved, and a model that falsifies it is available.
      --
+     -- The 'WE.GroundEvalFn' is only available for use during the execution of
+     -- a 'ProofConsumer'. See 'WSA.SolverAdapter'.
+     --
      -- Corresponds to 'W4R.Sat'.
    | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
      -- | The SMT solver returned \"unknown\".
@@ -47,25 +140,84 @@ data ProofResult sym t
      -- Corresponds to 'W4R.Unknown'.
    | Unknown
 
--- | Prove a single goal ('CB.Assertion') under the supplied 'Assumptions'.
---
--- The overall approach is:
---
--- * Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
---   from branch conditions).
--- * Negate the goal ('CB.Assertion') that were are trying to prove.
--- * Attempt to prove the conjunction of the assumptions and the negated goal.
---
--- If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample
--- that makes the original goal false, so we have disproven the goal. If the
--- negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the
--- original goal is proven.
+-- | A 'ProofStrategy' dictates how results are proved.
+data ProofStrategy sym m t r
+  = ProofStrategy
+    { -- | Generally 'offlineProver' or 'onlineProver'
+      stratProver :: {-# UNPACK #-} !(Prover sym m t r)
+    , stratCombine :: Combiner m r
+    }
+
+-- | A callback used to consume a 'ProofResult'.
 --
--- Another way to think of this is as the negated material conditional
--- (implication) @not (assumptions -> assertion)@. This formula is equivalent
--- to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not
--- assertion)@.
-proveGoal ::
+-- If the result is 'Disproved', then this function must consume the
+-- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.
+newtype ProofConsumer sym t r
+  = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)
+
+---------------------------------------------------------------------
+-- *** Combiner
+
+data SubgoalResult r
+  = SubgoalResult
+    { subgoalWasProved :: !Bool
+    , subgoalResult :: !r
+    }
+
+newtype Combiner m r
+  = Combiner
+    { getCombiner ::
+        m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
+    }
+
+keepGoing :: Monad m => Semigroup r => Combiner m r
+keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2
+  where
+  subgoalAnd ::
+    Semigroup r =>
+    SubgoalResult r ->
+    SubgoalResult r ->
+    SubgoalResult r
+  subgoalAnd (SubgoalResult ok1 r1) (SubgoalResult ok2 r2) =
+    SubgoalResult (ok1 && ok2) (r1 <> r2)
+
+failFast :: Monad m => Semigroup r => Combiner m r
+failFast = Combiner $ \sr1 sr2 -> do
+  SubgoalResult ok1 r1 <- sr1
+  if ok1
+  then do
+    SubgoalResult ok2 r2 <- sr2
+    pure (SubgoalResult ok2 (r1 <> r2))
+  else pure (SubgoalResult False r1)
+
+isProved :: ProofResult sym t -> Bool
+isProved =
+  \case
+    Proved {} -> True
+    Disproved {} -> False
+    Unknown {} -> False
+
+---------------------------------------------------------------------
+-- ** Prover
+
+data Prover sym m t r
+  = Prover
+    { proverProve ::
+        Assumptions sym ->
+        CB.Assertion sym ->
+        ProofConsumer sym t r ->
+        m (SubgoalResult r)
+    , proverAssume ::
+        Assumptions sym ->
+        m (SubgoalResult r) ->
+        m (SubgoalResult r)
+    }
+
+---------------------------------------------------------------------
+-- *** Offline
+
+offlineProve ::
+  MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
   sym ->
@@ -73,77 +225,132 @@ proveGoal ::
   WSA.SolverAdapter st ->
   Assumptions sym ->
   CB.Assertion sym ->
-  -- | Continuation to process the 'ProofResult'.
-  (CB.ProofObligation sym -> ProofResult sym t -> IO r) ->
-  IO r
-proveGoal sym ld adapter asms goal k = do
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProve sym ld adapter asmps goal (ProofConsumer k) = liftIO $ do
   let goalPred = goal ^. CB.labeledPred
-  asmsPred <- CB.assumptionsPred sym asms
+  asmsPred <- CB.assumptionsPred sym asmps
   notGoal <- W4.notPred sym goalPred
-  WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $
-    k (CB.ProofGoal asms goal) .
-      \case
-        W4R.Sat (gfn, binds) -> Disproved gfn binds
-        W4R.Unsat () -> Proved
-        W4R.Unknown -> Unknown
-
--- | Prove a single 'CB.ProofGoal'.
-proveProofGoal ::
+  WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ \r ->
+    let r' =
+          case r of
+            W4R.Sat (gfn, binds) -> Disproved gfn binds
+            W4R.Unsat () -> Proved
+            W4R.Unknown -> Unknown
+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
+
+offlineProver ::
+  MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
   sym ->
   WSA.LogData ->
   WSA.SolverAdapter st ->
-  CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) ->
-  -- | Continuation to process the 'ProofResult'.
-  (CB.ProofObligation sym -> ProofResult sym t -> IO r) ->
-  IO r
-proveProofGoal sym ld adapter (CB.ProofGoal asms goal) =
-  proveGoal sym ld adapter asms goal
-
--- | Prove a collection of 'CB.Goals'.
-proveGoals ::
-  (Monoid m, sym ~ WE.ExprBuilder t st fs) =>
+  Prover sym m t r
+offlineProver sym ld adapter =
+  Prover
+  { proverProve = offlineProve sym ld adapter
+  , proverAssume = \_asmps a -> a
+  }
+
+---------------------------------------------------------------------
+-- *** Online
+
+onlineProve ::
+  MonadIO m =>
+  W4SMT.SMTReadWriter solver =>
+  (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
+  WPO.SolverProcess t solver ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+onlineProve sProc asmps goal (ProofConsumer k) =
+  liftIO $ WPO.checkSatisfiableWithModel sProc "prove" (goal ^. CB.labeledPred) $ \r ->
+    let r' =
+          case r of
+            W4R.Sat gfn -> Disproved gfn Nothing
+            W4R.Unsat () -> Proved
+            W4R.Unknown -> Unknown
+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
+
+onlineAssume :: 
+  MonadIO m =>
+  MonadMask m =>
+  W4SMT.SMTReadWriter solver =>
+  W4.IsSymExprBuilder sym =>
+  (W4.SymExpr sym ~ WE.Expr t) =>
   sym ->
-  WSA.LogData ->
-  WSA.SolverAdapter st ->
+  WPO.SolverProcess t solver ->
+  Assumptions sym ->
+  m r ->
+  m r
+onlineAssume sym sProc asmps a =
+  WPO.inNewFrame sProc $ do
+    liftIO $ do
+      let conn = WPO.solverConn sProc
+      asmpsPred <- CB.assumptionsPred sym asmps
+      term <- W4SMT.mkFormula conn asmpsPred
+      W4SMT.assumeFormula conn term
+      pure ()
+    a
+
+onlineProver ::
+  MonadIO m =>
+  MonadMask m =>
+  W4SMT.SMTReadWriter solver =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WPO.SolverProcess t solver ->
+  Prover sym m t r
+onlineProver sym sProc =
+  Prover
+  { proverProve = onlineProve sProc
+  , proverAssume = onlineAssume sym sProc
+  }
+
+---------------------------------------------------------------------
+-- * Proving goals
+
+proveGoals ::
+  Functor m =>
+  ProofStrategy sym m t r ->
   CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
-  -- | Continuation to process each 'ProofResult'.
-  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
-  IO m
-proveGoals sym ld adapter goals k =
-  getConst $
-    traverseGoalsWithAssumptions
-      (\as g -> Const (proveGoal sym ld adapter as g k))
+  ProofConsumer sym t r ->
+  m r
+proveGoals (ProofStrategy prover (Combiner comb)) goals k =
+  fmap subgoalResult $
+    consumeGoalsWithAssumptions
+      (\asmps gl -> proverProve prover asmps gl k)
+      comb
       goals
 
--- | Prove a collection of 'CB.ProofObligations'.
 proveObligations ::
-  (Monoid m, sym ~ WE.ExprBuilder t st fs) =>
-  sym ->
-  WSA.LogData ->
-  WSA.SolverAdapter st ->
+  Applicative m =>
+  Monoid r =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  ProofStrategy sym m t r ->
   CB.ProofObligations sym ->
-  -- | Continuation to process each 'ProofResult'.
-  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
-  IO m
-proveObligations sym ld adapter obligations k =
+  ProofConsumer sym t r ->
+  m r
+proveObligations strat obligations k =
   case obligations of
     Nothing -> pure mempty
-    Just goals -> proveGoals sym ld adapter goals k
+    Just goals -> proveGoals strat goals k
 
 -- | Prove a the current collection of 'CB.ProofObligations' associated with the
 -- symbolic backend (retrieved via 'CB.getProofObligations').
 proveCurrentObligations ::
-  (Monoid m, CB.IsSymBackend sym bak, sym ~ WE.ExprBuilder t st fs) =>
+  MonadIO m =>
+  Monoid r =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  CB.IsSymBackend sym bak =>
   bak ->
-  WSA.LogData ->
-  WSA.SolverAdapter st ->
-  -- | Continuation to process each 'ProofResult'.
-  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
-  IO m
-proveCurrentObligations bak ld adapter k = do
-  obligations <- CB.getProofObligations bak
-  let sym = CB.backendGetSym bak
-  proveObligations sym ld adapter obligations k
+  ProofStrategy sym m t r ->
+  ProofConsumer sym t r ->
+  m r
+proveCurrentObligations bak strat k = do
+  obligations <- liftIO (CB.getProofObligations bak)
+  proveObligations strat obligations k

From 63a560f37fa6ea1b23ac796a4436765b16f8cffa Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 25 Jun 2024 10:54:03 -0400
Subject: [PATCH 02/16] Add timeouts to obligation proving

---
 crucible-cli/src/Lang/Crucible/CLI.hs         | 15 ++++-
 crucible-symio/tests/TestMain.hs              | 12 +++-
 .../src/Lang/Crucible/Syntax/Overrides.hs     | 12 +++-
 crucible/crucible.cabal                       |  3 +
 crucible/src/Lang/Crucible/Backend/Prove.hs   | 49 ++++++++++++++--
 crucible/src/Lang/Crucible/Utils/Seconds.hs   | 18 ++++++
 crucible/src/Lang/Crucible/Utils/Timeout.hs   | 58 +++++++++++++++++++
 7 files changed, 154 insertions(+), 13 deletions(-)
 create mode 100644 crucible/src/Lang/Crucible/Utils/Seconds.hs
 create mode 100644 crucible/src/Lang/Crucible/Utils/Timeout.hs

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index 137c4fe4d..e75ef1e2c 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -21,7 +21,7 @@ module Lang.Crucible.CLI
   ) where
 
 import Control.Monad
-
+import Control.Monad.Except (runExceptT)
 import Data.Foldable
 import Data.Map (Map)
 import Data.Text (Text)
@@ -54,6 +54,8 @@ import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import What4.Config
 import What4.Interface (getConfiguration)
@@ -181,14 +183,21 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        getProofObligations bak >>= \case
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
                          Just {} -> hPutStrLn outh "==== Proof obligations ===="
-                       let prover = Prove.offlineProver sym defaultLogData z3Adapter
+                       -- TODO: Make this timeout configurable via the CLI
+                       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+                       let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter
                        let strat = Prove.ProofStrategy prover Prove.keepGoing
-                       Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
+                       merr <- runExceptT $ Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
                          hPrint outh =<< ppProofObligation sym goal
                          case res of
                            Prove.Proved {} -> hPutStrLn outh "PROVED"
                            Prove.Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
                            Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
+                       case merr of
+                         Left CTO.TimedOut -> hPutStrLn outh $ unlines ["TIMEOUT"]
+                         Left (CTO.Exception exn) ->
+                          hPutStrLn outh $ unlines ["EXCEPTION", show exn]
+                         Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"
 
diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs
index e390a7b5e..474bdcfff 100644
--- a/crucible-symio/tests/TestMain.hs
+++ b/crucible-symio/tests/TestMain.hs
@@ -27,6 +27,7 @@ import           GHC.TypeNats
 import           Control.Lens ( (^.) )
 
 import           Control.Monad (foldM )
+import           Control.Monad.Except (runExceptT)
 import           Control.Monad.IO.Class (liftIO)
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
@@ -51,6 +52,8 @@ import qualified Lang.Crucible.Simulator as CS
 import qualified Lang.Crucible.Simulator.OverrideSim as CSO
 import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator.GlobalState as CGS
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
@@ -134,9 +137,10 @@ runFSTest' bak (FSTest fsTest) = do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
 
-  let prover = CB.offlineProver sym WSA.defaultLogData W4Y.yicesAdapter
+  let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+  let prover = CB.offlineProver timeout sym WSA.defaultLogData W4Y.yicesAdapter
   let strat = CB.ProofStrategy prover CB.failFast
-  CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
+  merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
     \case
       CB.Proved {} -> return ()
       CB.Unknown {} -> T.assertFailure "Inconclusive"
@@ -147,6 +151,10 @@ runFSTest' bak (FSTest fsTest) = do
         putStrLn (showF asmsPred)
         putStrLn (showF goalPred)
         T.assertFailure "Assertion Failure"
+  case merr of
+    Left CTO.TimedOut -> T.assertFailure "Timeout"
+    Left (CTO.Exception exn) -> T.assertFailure ("Exception: " ++ show exn)
+    Right () -> pure ()
 
 showAbortedResult :: CS.AbortedResult c d -> String
 showAbortedResult ar = case ar of
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index 1f749e011..76933c266 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -10,6 +10,7 @@ module Lang.Crucible.Syntax.Overrides
   ) where
 
 import Control.Lens hiding ((:>), Empty)
+import Control.Monad.Except (runExceptT)
 import Control.Monad.IO.Class
 import System.IO
 
@@ -25,6 +26,8 @@ import qualified Lang.Crucible.Backend.Prove as CB
 import Lang.Crucible.Types
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 
 setupOverrides ::
@@ -48,12 +51,17 @@ proveObligations =
 
        let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
                                     , logReason = "assertion proof" }
-       let prover = CB.offlineProver sym logData z3Adapter
+       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+       let prover = CB.offlineProver timeout sym logData z3Adapter
        let strat = CB.ProofStrategy prover CB.keepGoing
-       CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
+       merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
          \case
            CB.Proved {}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
            CB.Disproved {} -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
            CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       case merr of
+         Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
+         Left (CTO.Exception exn) -> hPutStrLn h $ unlines ["Exception during proof!", show exn]
+         Right () -> pure ()
 
        clearProofObligations bak
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index c778eca6b..c786a4e23 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -44,6 +44,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
+    async,
     base >= 4.13 && < 4.19,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
@@ -129,6 +130,8 @@ library
     Lang.Crucible.Utils.MuxTree
     Lang.Crucible.Utils.PrettyPrint
     Lang.Crucible.Utils.RegRewrite
+    Lang.Crucible.Utils.Seconds
+    Lang.Crucible.Utils.Timeout
     Lang.Crucible.Utils.StateContT
     Lang.Crucible.Utils.Structural
 
diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 2d6196658..fb971dad0 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -58,6 +58,7 @@ module Lang.Crucible.Backend.Prove
   , Prover(..)
     -- *** Offline
   , offlineProve
+  , offlineProveWithTimeout
   , offlineProver
     -- *** Online
   , onlineProve
@@ -70,6 +71,7 @@ module Lang.Crucible.Backend.Prove
 
 import           Control.Lens ((^.))
 import           Control.Monad.Catch (MonadMask)
+import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
 import qualified Control.Monad.Reader as Reader
 
@@ -82,6 +84,8 @@ import qualified What4.Solver.Adapter as WSA
 
 import qualified Lang.Crucible.Backend as CB
 import           Lang.Crucible.Backend.Assumptions (Assumptions)
+import           Lang.Crucible.Utils.Timeout (Timeout, TimeoutError)
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 -- | Local helper
 consumeGoals ::
@@ -216,8 +220,8 @@ data Prover sym m t r
 ---------------------------------------------------------------------
 -- *** Offline
 
-offlineProve ::
-  MonadIO m =>
+-- Not exported
+offlineProveIO ::
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
   sym ->
@@ -226,8 +230,8 @@ offlineProve ::
   Assumptions sym ->
   CB.Assertion sym ->
   ProofConsumer sym t r ->
-  m (SubgoalResult r)
-offlineProve sym ld adapter asmps goal (ProofConsumer k) = liftIO $ do
+  IO (SubgoalResult r)
+offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do
   let goalPred = goal ^. CB.labeledPred
   asmsPred <- CB.assumptionsPred sym asmps
   notGoal <- W4.notPred sym goalPred
@@ -239,17 +243,50 @@ offlineProve sym ld adapter asmps goal (ProofConsumer k) = liftIO $ do
             W4R.Unknown -> Unknown
     in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
 
+offlineProve ::
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProve sym ld adapter asmps goal k =
+  liftIO (offlineProveIO sym ld adapter asmps goal k)
+
+offlineProveWithTimeout ::
+  MonadError TimeoutError m =>
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  Timeout ->
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProveWithTimeout to sym ld adapter asmps goal k = do
+  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
+  liftEither r
+
 offlineProver ::
+  MonadError TimeoutError m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
+  Timeout ->
   W4.IsSymExprBuilder sym =>
   sym ->
   WSA.LogData ->
   WSA.SolverAdapter st ->
   Prover sym m t r
-offlineProver sym ld adapter =
+offlineProver to sym ld adapter =
   Prover
-  { proverProve = offlineProve sym ld adapter
+  { proverProve = offlineProveWithTimeout to sym ld adapter
   , proverAssume = \_asmps a -> a
   }
 
diff --git a/crucible/src/Lang/Crucible/Utils/Seconds.hs b/crucible/src/Lang/Crucible/Utils/Seconds.hs
new file mode 100644
index 000000000..1350ce44b
--- /dev/null
+++ b/crucible/src/Lang/Crucible/Utils/Seconds.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Lang.Crucible.Utils.Seconds
+  ( Seconds
+  , secondsToInt
+  , secondsFromInt
+  , secondsToMicroseconds
+  ) where
+
+newtype Seconds = Seconds { secondsToInt :: Int }
+  deriving (Eq, Num, Ord, Show)
+
+-- | Inverse of 'secondsToInt'
+secondsFromInt :: Int -> Seconds
+secondsFromInt = Seconds
+
+secondsToMicroseconds :: Seconds -> Int
+secondsToMicroseconds = (* 1000000) . secondsToInt
diff --git a/crucible/src/Lang/Crucible/Utils/Timeout.hs b/crucible/src/Lang/Crucible/Utils/Timeout.hs
new file mode 100644
index 000000000..2f682720f
--- /dev/null
+++ b/crucible/src/Lang/Crucible/Utils/Timeout.hs
@@ -0,0 +1,58 @@
+module Lang.Crucible.Utils.Timeout
+  ( Timeout(..)
+  , TimeoutError(..)
+  , withTimeout
+  ) where
+
+import qualified Control.Concurrent as CC
+import qualified Control.Concurrent.Async as CCA
+import           Control.Exception.Base (SomeException)
+
+import qualified Lang.Crucible.Utils.Seconds as Secs
+
+-- | A timeout, in seconds.
+newtype Timeout = Timeout { getTimeout :: Secs.Seconds }
+  deriving (Eq, Ord, Show)
+
+-- Private, not exported
+timeoutToMicros :: Timeout -> Int
+timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
+
+-- Private, not exported
+data DidTimeOut = DidTimeOut
+
+-- | An error resulting from 'withTimeout'.
+data TimeoutError
+  = -- | The task timed out
+    TimedOut
+    -- | Some other exception ocurred
+  | Exception SomeException
+  deriving Show
+
+-- | Execute a task with a timeout.
+--
+-- Catches any exceptions that occur during the task, returning them as
+-- @'Left' ('Exception' exn)@.
+withTimeout ::
+  -- | Timeout duration (seconds)
+  Timeout ->
+  -- | Task to attempt
+  IO a ->
+  IO (Either TimeoutError a)
+withTimeout to task = do
+  worker <- CCA.async task
+  timeout <- CCA.async $ do
+    CC.threadDelay (timeoutToMicros to)
+    CCA.cancel worker
+    return DidTimeOut
+  res <- CCA.waitEitherCatch timeout worker
+  case res of
+    Left (Right DidTimeOut) -> do
+      return (Left TimedOut)
+    Left (Left exn) -> do
+      return (Left (Exception exn))
+    Right (Left exn) -> do
+      return (Left (Exception exn))
+    Right (Right val) ->
+      return (Right val)
+

From ae52603a6dda4a5a15ce241d293f4bba5b6ad36a Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 25 Jun 2024 11:01:45 -0400
Subject: [PATCH 03/16] Simplify obligation-proving timeouts by not catching
 exceptions

---
 crucible-cli/src/Lang/Crucible/CLI.hs         |  2 -
 crucible-symio/tests/TestMain.hs              |  1 -
 .../src/Lang/Crucible/Syntax/Overrides.hs     |  1 -
 crucible/src/Lang/Crucible/Backend/Prove.hs   |  6 +--
 crucible/src/Lang/Crucible/Utils/Timeout.hs   | 40 +++++--------------
 5 files changed, 13 insertions(+), 37 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index e75ef1e2c..bcfbb27bf 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -195,8 +195,6 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                            Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
                        case merr of
                          Left CTO.TimedOut -> hPutStrLn outh $ unlines ["TIMEOUT"]
-                         Left (CTO.Exception exn) ->
-                          hPutStrLn outh $ unlines ["EXCEPTION", show exn]
                          Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"
diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs
index 474bdcfff..67d7720fe 100644
--- a/crucible-symio/tests/TestMain.hs
+++ b/crucible-symio/tests/TestMain.hs
@@ -153,7 +153,6 @@ runFSTest' bak (FSTest fsTest) = do
         T.assertFailure "Assertion Failure"
   case merr of
     Left CTO.TimedOut -> T.assertFailure "Timeout"
-    Left (CTO.Exception exn) -> T.assertFailure ("Exception: " ++ show exn)
     Right () -> pure ()
 
 showAbortedResult :: CS.AbortedResult c d -> String
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index 76933c266..e9a293149 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -61,7 +61,6 @@ proveObligations =
            CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
        case merr of
          Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
-         Left (CTO.Exception exn) -> hPutStrLn h $ unlines ["Exception during proof!", show exn]
          Right () -> pure ()
 
        clearProofObligations bak
diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index fb971dad0..3ee211d2f 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -84,7 +84,7 @@ import qualified What4.Solver.Adapter as WSA
 
 import qualified Lang.Crucible.Backend as CB
 import           Lang.Crucible.Backend.Assumptions (Assumptions)
-import           Lang.Crucible.Utils.Timeout (Timeout, TimeoutError)
+import           Lang.Crucible.Utils.Timeout (Timeout, TimedOut)
 import qualified Lang.Crucible.Utils.Timeout as CTO
 
 -- | Local helper
@@ -258,7 +258,7 @@ offlineProve sym ld adapter asmps goal k =
   liftIO (offlineProveIO sym ld adapter asmps goal k)
 
 offlineProveWithTimeout ::
-  MonadError TimeoutError m =>
+  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
@@ -275,7 +275,7 @@ offlineProveWithTimeout to sym ld adapter asmps goal k = do
   liftEither r
 
 offlineProver ::
-  MonadError TimeoutError m =>
+  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   Timeout ->
diff --git a/crucible/src/Lang/Crucible/Utils/Timeout.hs b/crucible/src/Lang/Crucible/Utils/Timeout.hs
index 2f682720f..42a70a108 100644
--- a/crucible/src/Lang/Crucible/Utils/Timeout.hs
+++ b/crucible/src/Lang/Crucible/Utils/Timeout.hs
@@ -1,12 +1,11 @@
 module Lang.Crucible.Utils.Timeout
   ( Timeout(..)
-  , TimeoutError(..)
+  , TimedOut(..)
   , withTimeout
   ) where
 
 import qualified Control.Concurrent as CC
 import qualified Control.Concurrent.Async as CCA
-import           Control.Exception.Base (SomeException)
 
 import qualified Lang.Crucible.Utils.Seconds as Secs
 
@@ -18,41 +17,22 @@ newtype Timeout = Timeout { getTimeout :: Secs.Seconds }
 timeoutToMicros :: Timeout -> Int
 timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
 
--- Private, not exported
-data DidTimeOut = DidTimeOut
-
--- | An error resulting from 'withTimeout'.
-data TimeoutError
-  = -- | The task timed out
-    TimedOut
-    -- | Some other exception ocurred
-  | Exception SomeException
+-- | A task timed out.
+data TimedOut = TimedOut
   deriving Show
 
 -- | Execute a task with a timeout.
 --
--- Catches any exceptions that occur during the task, returning them as
--- @'Left' ('Exception' exn)@.
+-- Implemented via 'CCA.race', so re-throws exceptions that occur during the
+-- task (if it completes before the timeout).
 withTimeout ::
   -- | Timeout duration (seconds)
   Timeout ->
   -- | Task to attempt
   IO a ->
-  IO (Either TimeoutError a)
+  IO (Either TimedOut a)
 withTimeout to task = do
-  worker <- CCA.async task
-  timeout <- CCA.async $ do
-    CC.threadDelay (timeoutToMicros to)
-    CCA.cancel worker
-    return DidTimeOut
-  res <- CCA.waitEitherCatch timeout worker
-  case res of
-    Left (Right DidTimeOut) -> do
-      return (Left TimedOut)
-    Left (Left exn) -> do
-      return (Left (Exception exn))
-    Right (Left exn) -> do
-      return (Left (Exception exn))
-    Right (Right val) ->
-      return (Right val)
-
+  let timeout = do
+        CC.threadDelay (timeoutToMicros to)
+        pure TimedOut
+  CCA.race timeout task

From 6beaf4f3a163c7860920199a97987ab3b9dbf446 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 25 Jun 2024 12:01:58 -0400
Subject: [PATCH 04/16] Simplify some obligation-proving code

---
 crucible-cli/src/Lang/Crucible/CLI.hs         | 21 +++++++++++--------
 .../src/Lang/Crucible/Syntax/Overrides.hs     | 16 +++++++-------
 2 files changed, 21 insertions(+), 16 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index bcfbb27bf..3ad8171c5 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -187,15 +187,18 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        let timeout = CTO.Timeout (Sec.secondsFromInt 5)
                        let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter
                        let strat = Prove.ProofStrategy prover Prove.keepGoing
-                       merr <- runExceptT $ Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
-                         hPrint outh =<< ppProofObligation sym goal
-                         case res of
-                           Prove.Proved {} -> hPutStrLn outh "PROVED"
-                           Prove.Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
-                           Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
-                       case merr of
-                         Left CTO.TimedOut -> hPutStrLn outh $ unlines ["TIMEOUT"]
-                         Right () -> pure ()
+                       let ppResult =
+                             \case
+                               Prove.Proved {} ->  "PROVED"
+                               Prove.Disproved {} -> "COUNTEREXAMPLE"
+                               Prove.Unknown {} -> "UNKNOWN"
+                       let printer = Prove.ProofConsumer $ \goal res -> do
+                             hPrint outh =<< ppProofObligation sym goal
+                             hPutStrLn outh (ppResult res)
+                       runExceptT (Prove.proveCurrentObligations bak strat printer) >>=
+                         \case
+                           Left CTO.TimedOut -> hPutStrLn outh "TIMEOUT"
+                           Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"
 
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index e9a293149..0645296f2 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -54,13 +54,15 @@ proveObligations =
        let timeout = CTO.Timeout (Sec.secondsFromInt 5)
        let prover = CB.offlineProver timeout sym logData z3Adapter
        let strat = CB.ProofStrategy prover CB.keepGoing
-       merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
+       let ppResult o =
+             \case
+               CB.Proved {}  -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)
+       runExceptT (CB.proveCurrentObligations bak strat printer) >>=
          \case
-           CB.Proved {}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-           CB.Disproved {} -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-           CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-       case merr of
-         Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
-         Right () -> pure ()
+           Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
+           Right () -> pure ()
 
        clearProofObligations bak

From a41d50991d633339938155101b2924c57074d55d Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 25 Jun 2024 12:09:32 -0400
Subject: [PATCH 05/16] Haddocks for goal-proving helpers

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 33 +++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 3ee211d2f..b1fdf26f3 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -13,8 +13,10 @@ configurability, encapsulated in a 'ProofStrategy':
   solvers ('onlineProver') can share state as assumptions are added. See the
   top-level README for What4 for further discussion of this choice.
 * Failing fast ('failFast') vs. keeping going ('keepGoing')
-* Parallelism and timeouts: Not yet available via helpers in this module, but
-  may be added to a 'ProofStrategy' by clients.
+* Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without
+  ('offlineProve')
+* Parallelism: Not yet available via helpers in this module, but may be added to
+  a 'ProofStrategy' by clients.
 
 Once an appropriate strategy has been selected, it can be passed to entrypoints
 such as 'proveObligations' to dispatch proof obligations.
@@ -243,6 +245,12 @@ offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do
             W4R.Unknown -> Unknown
     in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
 
+-- | Prove a goal using an \"offline\" solver (i.e., one process per goal).
+--
+-- See 'offlineProveWithTimeout' for a version that integrates 'Timeout's.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
 offlineProve ::
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
@@ -257,6 +265,12 @@ offlineProve ::
 offlineProve sym ld adapter asmps goal k =
   liftIO (offlineProveIO sym ld adapter asmps goal k)
 
+-- | Prove a goal using an \"offline\" solver, with a timeout.
+--
+-- See 'offlineProveWithTimeout' for a version without 'Timeout's.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
 offlineProveWithTimeout ::
   MonadError TimedOut m =>
   MonadIO m =>
@@ -274,6 +288,10 @@ offlineProveWithTimeout to sym ld adapter asmps goal k = do
   r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
   liftEither r
 
+-- | Prove goals using 'offlineProveWithTimeout'.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
 offlineProver ::
   MonadError TimedOut m =>
   MonadIO m =>
@@ -293,6 +311,10 @@ offlineProver to sym ld adapter =
 ---------------------------------------------------------------------
 -- *** Online
 
+-- | Prove a goal using an \"online\" solver (i.e., one process for all goals).
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
 onlineProve ::
   MonadIO m =>
   W4SMT.SMTReadWriter solver =>
@@ -312,6 +334,7 @@ onlineProve sProc asmps goal (ProofConsumer k) =
             W4R.Unknown -> Unknown
     in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
 
+-- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame').
 onlineAssume :: 
   MonadIO m =>
   MonadMask m =>
@@ -333,6 +356,10 @@ onlineAssume sym sProc asmps a =
       pure ()
     a
 
+-- | Prove goals using 'onlineProve' and 'onlineAssume'.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
 onlineProver ::
   MonadIO m =>
   MonadMask m =>
@@ -351,6 +378,7 @@ onlineProver sym sProc =
 ---------------------------------------------------------------------
 -- * Proving goals
 
+-- | Prove a collection of 'CB.Goals' using the specified 'ProofStrategy'.
 proveGoals ::
   Functor m =>
   ProofStrategy sym m t r ->
@@ -364,6 +392,7 @@ proveGoals (ProofStrategy prover (Combiner comb)) goals k =
       comb
       goals
 
+-- | Prove a collection of 'CB.ProofObligations' using a 'ProofStrategy'.
 proveObligations ::
   Applicative m =>
   Monoid r =>

From a836bc3cafcbc26bb3a87d365c3b23a8fb59dcae Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 26 Jun 2024 11:56:41 -0400
Subject: [PATCH 06/16] Proving goals in parallel

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 42 +++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index b1fdf26f3..e0eca79c2 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -45,6 +45,7 @@ assertion)@.
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Lang.Crucible.Backend.Prove
   ( -- * Strategy
@@ -71,11 +72,16 @@ module Lang.Crucible.Backend.Prove
   , proveCurrentObligations
   ) where
 
+import qualified Control.Concurrent as CC
+import qualified Control.Concurrent.Async as CCA
+import qualified Control.Concurrent.QSem as CCQ
+import qualified Control.Exception as X
 import           Control.Lens ((^.))
 import           Control.Monad.Catch (MonadMask)
 import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
 import qualified Control.Monad.Reader as Reader
+import qualified Data.IORef as IORef
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
@@ -123,6 +129,26 @@ consumeGoalsWithAssumptions onGoal onConj goals =
       (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
       (\g1 g2 -> onConj <$> g1 <*> g2)
 
+consumeGoalsParallel ::
+  Monoid asmp =>
+  -- | Consume a 'Prove'
+  (asmp -> goal -> IO a) ->
+  -- | Consume a 'ProveConj'
+  (IO () -> IO () -> IO ()) ->
+  CB.Goals asmp goal ->
+  IO [a]
+consumeGoalsParallel onGoal onConj goals = do
+  caps <- CC.getNumCapabilities
+  sem <- liftIO $ CCQ.newQSem caps
+  workers <- liftIO $ IORef.newIORef []
+  let onGoal' asmps goal = do
+        let withQSem = X.bracket_ (CCQ.waitQSem sem) (CCQ.signalQSem sem) 
+        task' <- CCA.async (withQSem (onGoal asmps goal))
+        IORef.modifyIORef' workers (task':)
+        pure ()
+  consumeGoalsWithAssumptions onGoal' onConj goals
+  mapM CCA.wait =<< IORef.readIORef workers
+
 ---------------------------------------------------------------------
 -- * Strategy
 
@@ -420,3 +446,19 @@ proveCurrentObligations ::
 proveCurrentObligations bak strat k = do
   obligations <- liftIO (CB.getProofObligations bak)
   proveObligations strat obligations k
+
+---------------------------------------------------------------------
+-- * Parallelism
+
+proveGoalsInParallel ::
+  Semigroup r =>
+  ProofStrategy sym IO t r ->
+  ProofConsumer sym t r ->
+  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
+  IO [r]
+proveGoalsInParallel strat k goals =
+  map subgoalResult <$>
+    consumeGoalsParallel
+      (\asmps gl -> proverProve (stratProver strat) asmps gl k)
+      (>>)
+      goals

From cd99fcd8043a2decd9dff348089521e519b6e192 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 26 Jun 2024 15:21:37 -0400
Subject: [PATCH 07/16] Better parallel proving

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 128 +++++++++++++++++---
 1 file changed, 111 insertions(+), 17 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index e0eca79c2..cfad9160f 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -4,23 +4,32 @@ Description : Proving goals under assumptions
 Copyright   : (c) Galois, Inc 2024
 License     : BSD3
 
-This module contains helpers to dispatch the proof obligations arising from
-symbolic execution using SMT solvers. There are several dimensions of
-configurability, encapsulated in a 'ProofStrategy':
+== Overview
+
+The functions in this module dispatch proof obligations arising from symbolic
+execution using SMT solvers. There are several dimensions of configurability,
+encapsulated in a 'ProofStrategy':
 
 * Offline vs. online: Offline solvers ('offlineProver') are simpler to manage
-  and more easily parallelized, but starting processes adds overhead, and online
+  and more easily parallelized, but starting processes adds overhead; online
   solvers ('onlineProver') can share state as assumptions are added. See the
   top-level README for What4 for further discussion of this choice.
 * Failing fast ('failFast') vs. keeping going ('keepGoing')
 * Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without
   ('offlineProve')
-* Parallelism: Not yet available via helpers in this module, but may be added to
-  a 'ProofStrategy' by clients.
 
 Once an appropriate strategy has been selected, it can be passed to entrypoints
 such as 'proveObligations' to dispatch proof obligations.
 
+== Parallelism
+
+Parallel proving is available via a separate set of entrypoints, e.g,
+'proveGoalsInParallel'. It only makes sense to use these with offline 'Prover's.
+Furthermore, these can only be used with 'ProofStrategy's that operate in the
+'IO' monad.
+
+== Proving goals
+
 When proving a single goal, the overall approach is:
 
 * Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
@@ -70,6 +79,10 @@ module Lang.Crucible.Backend.Prove
   , proveGoals
   , proveObligations
   , proveCurrentObligations
+    -- * Proving goals in parallel
+  , proveGoalsInParallel
+  , proveObligationsInParallel
+  , proveCurrentObligationsInParallel
   ) where
 
 import qualified Control.Concurrent as CC
@@ -77,6 +90,7 @@ import qualified Control.Concurrent.Async as CCA
 import qualified Control.Concurrent.QSem as CCQ
 import qualified Control.Exception as X
 import           Control.Lens ((^.))
+import           Control.Monad (foldM)
 import           Control.Monad.Catch (MonadMask)
 import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
@@ -129,14 +143,15 @@ consumeGoalsWithAssumptions onGoal onConj goals =
       (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
       (\g1 g2 -> onConj <$> g1 <*> g2)
 
+-- | Not exported, but see 'proveGoalsInParallel'
 consumeGoalsParallel ::
   Monoid asmp =>
   -- | Consume a 'Prove'
-  (asmp -> goal -> IO a) ->
+  (asmp -> goal -> IO r) ->
   -- | Consume a 'ProveConj'
-  (IO () -> IO () -> IO ()) ->
+  (r -> r -> IO r) ->
   CB.Goals asmp goal ->
-  IO [a]
+  IO r
 consumeGoalsParallel onGoal onConj goals = do
   caps <- CC.getNumCapabilities
   sem <- liftIO $ CCQ.newQSem caps
@@ -146,8 +161,48 @@ consumeGoalsParallel onGoal onConj goals = do
         task' <- CCA.async (withQSem (onGoal asmps goal))
         IORef.modifyIORef' workers (task':)
         pure ()
-  consumeGoalsWithAssumptions onGoal' onConj goals
-  mapM CCA.wait =<< IORef.readIORef workers
+  consumeGoalsWithAssumptions onGoal' (>>) goals
+  go onConj =<< IORef.readIORef workers
+  where
+    go :: (r -> r -> IO r) -> [CCA.Async r] -> IO r
+    go combine tasks =
+      partitionPoll tasks >>=
+        \case
+          ([], []) -> error "Impossible"
+          ([], rest) -> delay >> go combine rest
+          ((r:rs), rest) -> do
+            accum <- foldM combine r rs
+            foldMReady combine accum rest
+  
+    -- Pause for 0.1 s = 1 * 10^5 microsecs
+    delay = do
+      let pointOneSecond = 100000
+      CC.threadDelay pointOneSecond
+
+    -- Like foldl', but processes the inputs whenever they're ready, rather than
+    -- in the order in which they're supplied in the list. Polls repeatedly, but
+    -- with a delay.
+    foldMReady :: (b -> a -> IO b) -> b -> [CCA.Async a] -> IO b
+    foldMReady f accum as = do
+      (ready, rest) <- partitionPoll as
+      result <- foldM f accum ready
+      if null rest
+      then pure result
+      else do
+        delay
+        foldMReady f result rest
+
+    -- Partition a list of tasks into those that are ready (in which case,
+    -- extract their results), and those that are still in progress.
+    partitionPoll :: [CCA.Async r] -> IO ([r], [CCA.Async r])
+    partitionPoll [] = pure ([], [])
+    partitionPoll (x:xs) = do
+      (ready, waiting) <- partitionPoll xs
+      CCA.poll x >>=
+        \case
+          Just (Left exn) -> X.throwIO exn
+          Just (Right r) -> pure (r:ready, waiting)
+          Nothing -> pure (ready, x:waiting)
 
 ---------------------------------------------------------------------
 -- * Strategy
@@ -448,17 +503,56 @@ proveCurrentObligations bak strat k = do
   proveObligations strat obligations k
 
 ---------------------------------------------------------------------
--- * Parallelism
+-- * Proving goals in parallel
 
+-- | Prove a collection of 'CB.Goals' using the specified offline
+-- 'ProofStrategy'.
+--
+-- TODO: details!
 proveGoalsInParallel ::
   Semigroup r =>
+  -- | Strategy with offline prover (e.g., 'offlineProver')
   ProofStrategy sym IO t r ->
-  ProofConsumer sym t r ->
   CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
-  IO [r]
-proveGoalsInParallel strat k goals =
-  map subgoalResult <$>
+  ProofConsumer sym t r ->
+  IO r
+proveGoalsInParallel strat goals k =
+  subgoalResult <$>
     consumeGoalsParallel
       (\asmps gl -> proverProve (stratProver strat) asmps gl k)
-      (>>)
+      (\r1 r2 -> getCombiner (stratCombine strat) (pure r1) (pure r2))
       goals
+
+-- | Prove a collection of 'CB.ProofObligations' in parallel using an offline
+-- 'ProofStrategy'.
+--
+-- For more details, see 'proveGoalsInParallel'.
+proveObligationsInParallel ::
+  Monoid r =>
+  -- | Strategy with offline prover (e.g., 'offlineProver')
+  ProofStrategy sym IO t r ->
+  CB.ProofObligations sym ->
+  ProofConsumer sym t r ->
+  IO r
+proveObligationsInParallel strat obligations k =
+  case obligations of
+    Nothing -> pure mempty
+    Just goals -> proveGoalsInParallel strat goals k
+
+-- | Prove a the current collection of 'CB.ProofObligations' associated with the
+-- symbolic backend (retrieved via 'CB.getProofObligations') in parallel using
+-- an offline 'ProofStrategy'.
+--
+-- For more details, see 'proveGoalsInParallel'.
+proveCurrentObligationsInParallel ::
+  Monoid r =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  CB.IsSymBackend sym bak =>
+  bak ->
+  -- | Strategy with offline prover (e.g., 'offlineProver')
+  ProofStrategy sym IO t r ->
+  ProofConsumer sym t r ->
+  IO r
+proveCurrentObligationsInParallel bak strat k = do
+  obligations <- liftIO (CB.getProofObligations bak)
+  proveObligationsInParallel strat obligations k

From 8efa109dfe37db7730a8c41fcbd49bea1db23543 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 26 Jun 2024 16:04:28 -0400
Subject: [PATCH 08/16] Further improvements to parallel proving

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 39 +++++++++++++++++----
 crucible/src/Lang/Crucible/Utils/Timeout.hs |  3 ++
 2 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index cfad9160f..f181914c5 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -71,6 +71,7 @@ module Lang.Crucible.Backend.Prove
     -- *** Offline
   , offlineProve
   , offlineProveWithTimeout
+  , offlineProveWithTimeoutIO
   , offlineProver
     -- *** Online
   , onlineProve
@@ -168,7 +169,9 @@ consumeGoalsParallel onGoal onConj goals = do
     go combine tasks =
       partitionPoll tasks >>=
         \case
-          ([], []) -> error "Impossible"
+          -- Note that `rest` can't be empty (and thus this cant loop
+          -- indefinitely), because `tasks` can't be empty, because `Goal`
+          -- is the only leaf of `Goals` (so there must be at least one).
           ([], rest) -> delay >> go combine rest
           ((r:rs), rest) -> do
             accum <- foldM combine r rs
@@ -348,7 +351,7 @@ offlineProve sym ld adapter asmps goal k =
 
 -- | Prove a goal using an \"offline\" solver, with a timeout.
 --
--- See 'offlineProveWithTimeout' for a version without 'Timeout's.
+-- See 'offlineProve' for a version without 'Timeout's.
 --
 -- See the module-level documentation for further discussion of offline vs.
 -- online solving.
@@ -369,12 +372,31 @@ offlineProveWithTimeout to sym ld adapter asmps goal k = do
   r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
   liftEither r
 
--- | Prove goals using 'offlineProveWithTimeout'.
+-- | Like 'offlineProverWithTimeout', but throws timeouts as exceptions using
+-- 'X.throwIO' instead of requiring 'MonadError'.
+offlineProveWithTimeoutIO ::
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  Timeout ->
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProveWithTimeoutIO to sym ld adapter asmps goal k = do
+  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
+  case r of
+    Left CTO.TimedOut -> liftIO (X.throwIO CTO.TimedOut)
+    Right r' -> pure r'
+
+-- | Prove goals using 'offlineProveWithTimeoutIO'.
 --
 -- See the module-level documentation for further discussion of offline vs.
 -- online solving.
 offlineProver ::
-  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   Timeout ->
@@ -385,7 +407,7 @@ offlineProver ::
   Prover sym m t r
 offlineProver to sym ld adapter =
   Prover
-  { proverProve = offlineProveWithTimeout to sym ld adapter
+  { proverProve = offlineProveWithTimeoutIO to sym ld adapter
   , proverAssume = \_asmps a -> a
   }
 
@@ -508,7 +530,12 @@ proveCurrentObligations bak strat k = do
 -- | Prove a collection of 'CB.Goals' using the specified offline
 -- 'ProofStrategy'.
 --
--- TODO: details!
+-- This function ensures that at most 'CC.getNumCapabilities' solvers are
+-- running at once. It first creates async tasks (with 'CCA.async') for proving
+-- each goal, then repeatedly polls them (with a delay of 0.1s), combining
+-- results (with the 'Combiner') as they become available. It does not support
+-- \"failing fast\", it always waits for all solvers to complete before
+-- returning.
 proveGoalsInParallel ::
   Semigroup r =>
   -- | Strategy with offline prover (e.g., 'offlineProver')
diff --git a/crucible/src/Lang/Crucible/Utils/Timeout.hs b/crucible/src/Lang/Crucible/Utils/Timeout.hs
index 42a70a108..c5ae04eba 100644
--- a/crucible/src/Lang/Crucible/Utils/Timeout.hs
+++ b/crucible/src/Lang/Crucible/Utils/Timeout.hs
@@ -6,6 +6,7 @@ module Lang.Crucible.Utils.Timeout
 
 import qualified Control.Concurrent as CC
 import qualified Control.Concurrent.Async as CCA
+import qualified Control.Exception as X
 
 import qualified Lang.Crucible.Utils.Seconds as Secs
 
@@ -21,6 +22,8 @@ timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
 data TimedOut = TimedOut
   deriving Show
 
+instance X.Exception TimedOut where
+
 -- | Execute a task with a timeout.
 --
 -- Implemented via 'CCA.race', so re-throws exceptions that occur during the

From 09f1800355496a3bb958331bf53f76986428859a Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 26 Jun 2024 17:03:37 -0400
Subject: [PATCH 09/16] More Haddocks for proving goals

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index f181914c5..d22ea9014 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -48,13 +48,13 @@ to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not
 assertion)@.
 -}
 
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.Backend.Prove
   ( -- * Strategy
@@ -248,18 +248,24 @@ newtype ProofConsumer sym t r
 ---------------------------------------------------------------------
 -- *** Combiner
 
+-- | Whether or not a subgoal was proved, together with the result from a
+-- 'ProofConsumer'.
 data SubgoalResult r
   = SubgoalResult
     { subgoalWasProved :: !Bool
     , subgoalResult :: !r
     }
+  deriving Functor
 
+-- | How to combine results of proofs, used as part of a 'ProofStrategy'.
 newtype Combiner m r
   = Combiner
     { getCombiner ::
         m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
     }
 
+-- | Combine 'SubgoalResult's using the '<>' operator. Keep going when subgoals
+-- fail.
 keepGoing :: Monad m => Semigroup r => Combiner m r
 keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2
   where
@@ -271,6 +277,8 @@ keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2
   subgoalAnd (SubgoalResult ok1 r1) (SubgoalResult ok2 r2) =
     SubgoalResult (ok1 && ok2) (r1 <> r2)
 
+-- | Combine 'SubgoalResult's using the '<>' operator. After the first subgoal
+-- fails, stop trying to prove further goals.
 failFast :: Monad m => Semigroup r => Combiner m r
 failFast = Combiner $ \sr1 sr2 -> do
   SubgoalResult ok1 r1 <- sr1
@@ -290,13 +298,16 @@ isProved =
 ---------------------------------------------------------------------
 -- ** Prover
 
+-- | A collection of functions used to prove goals as part of a 'ProofStrategy'.
 data Prover sym m t r
   = Prover
-    { proverProve ::
+    { -- | Prove a single goal under some 'Assumptions'.
+      proverProve ::
         Assumptions sym ->
         CB.Assertion sym ->
         ProofConsumer sym t r ->
         m (SubgoalResult r)
+      -- | Assume some 'Assumptions' in the scope of a subgoal.
     , proverAssume ::
         Assumptions sym ->
         m (SubgoalResult r) ->

From 50573aabe1f74541b7828a9d208aebe78d58f935 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 26 Jun 2024 17:12:45 -0400
Subject: [PATCH 10/16] Simplify an expression

---
 crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index 0645296f2..a7bab5612 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -62,7 +62,7 @@ proveObligations =
        let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)
        runExceptT (CB.proveCurrentObligations bak strat printer) >>=
          \case
-           Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
+           Left CTO.TimedOut -> hPutStrLn h "Proof timed out!"
            Right () -> pure ()
 
        clearProofObligations bak

From 83c9825067b02b84e3d03b0cf14b393253413dbc Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 1 Jul 2024 16:13:50 -0400
Subject: [PATCH 11/16] Revert "Further improvements to parallel proving"

This reverts commit 8efa109dfe37db7730a8c41fcbd49bea1db23543.
---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 39 ++++-----------------
 crucible/src/Lang/Crucible/Utils/Timeout.hs |  3 --
 2 files changed, 6 insertions(+), 36 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index d22ea9014..dc03383c0 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -71,7 +71,6 @@ module Lang.Crucible.Backend.Prove
     -- *** Offline
   , offlineProve
   , offlineProveWithTimeout
-  , offlineProveWithTimeoutIO
   , offlineProver
     -- *** Online
   , onlineProve
@@ -169,9 +168,7 @@ consumeGoalsParallel onGoal onConj goals = do
     go combine tasks =
       partitionPoll tasks >>=
         \case
-          -- Note that `rest` can't be empty (and thus this cant loop
-          -- indefinitely), because `tasks` can't be empty, because `Goal`
-          -- is the only leaf of `Goals` (so there must be at least one).
+          ([], []) -> error "Impossible"
           ([], rest) -> delay >> go combine rest
           ((r:rs), rest) -> do
             accum <- foldM combine r rs
@@ -362,7 +359,7 @@ offlineProve sym ld adapter asmps goal k =
 
 -- | Prove a goal using an \"offline\" solver, with a timeout.
 --
--- See 'offlineProve' for a version without 'Timeout's.
+-- See 'offlineProveWithTimeout' for a version without 'Timeout's.
 --
 -- See the module-level documentation for further discussion of offline vs.
 -- online solving.
@@ -383,31 +380,12 @@ offlineProveWithTimeout to sym ld adapter asmps goal k = do
   r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
   liftEither r
 
--- | Like 'offlineProverWithTimeout', but throws timeouts as exceptions using
--- 'X.throwIO' instead of requiring 'MonadError'.
-offlineProveWithTimeoutIO ::
-  MonadIO m =>
-  (sym ~ WE.ExprBuilder t st fs) =>
-  W4.IsSymExprBuilder sym =>
-  Timeout ->
-  sym ->
-  WSA.LogData ->
-  WSA.SolverAdapter st ->
-  Assumptions sym ->
-  CB.Assertion sym ->
-  ProofConsumer sym t r ->
-  m (SubgoalResult r)
-offlineProveWithTimeoutIO to sym ld adapter asmps goal k = do
-  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
-  case r of
-    Left CTO.TimedOut -> liftIO (X.throwIO CTO.TimedOut)
-    Right r' -> pure r'
-
--- | Prove goals using 'offlineProveWithTimeoutIO'.
+-- | Prove goals using 'offlineProveWithTimeout'.
 --
 -- See the module-level documentation for further discussion of offline vs.
 -- online solving.
 offlineProver ::
+  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   Timeout ->
@@ -418,7 +396,7 @@ offlineProver ::
   Prover sym m t r
 offlineProver to sym ld adapter =
   Prover
-  { proverProve = offlineProveWithTimeoutIO to sym ld adapter
+  { proverProve = offlineProveWithTimeout to sym ld adapter
   , proverAssume = \_asmps a -> a
   }
 
@@ -541,12 +519,7 @@ proveCurrentObligations bak strat k = do
 -- | Prove a collection of 'CB.Goals' using the specified offline
 -- 'ProofStrategy'.
 --
--- This function ensures that at most 'CC.getNumCapabilities' solvers are
--- running at once. It first creates async tasks (with 'CCA.async') for proving
--- each goal, then repeatedly polls them (with a delay of 0.1s), combining
--- results (with the 'Combiner') as they become available. It does not support
--- \"failing fast\", it always waits for all solvers to complete before
--- returning.
+-- TODO: details!
 proveGoalsInParallel ::
   Semigroup r =>
   -- | Strategy with offline prover (e.g., 'offlineProver')
diff --git a/crucible/src/Lang/Crucible/Utils/Timeout.hs b/crucible/src/Lang/Crucible/Utils/Timeout.hs
index c5ae04eba..42a70a108 100644
--- a/crucible/src/Lang/Crucible/Utils/Timeout.hs
+++ b/crucible/src/Lang/Crucible/Utils/Timeout.hs
@@ -6,7 +6,6 @@ module Lang.Crucible.Utils.Timeout
 
 import qualified Control.Concurrent as CC
 import qualified Control.Concurrent.Async as CCA
-import qualified Control.Exception as X
 
 import qualified Lang.Crucible.Utils.Seconds as Secs
 
@@ -22,8 +21,6 @@ timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
 data TimedOut = TimedOut
   deriving Show
 
-instance X.Exception TimedOut where
-
 -- | Execute a task with a timeout.
 --
 -- Implemented via 'CCA.race', so re-throws exceptions that occur during the

From 93f07b0be159b8800073e87aa108964f651d49e3 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 1 Jul 2024 16:13:58 -0400
Subject: [PATCH 12/16] Revert "Better parallel proving"

This reverts commit cd99fcd8043a2decd9dff348089521e519b6e192.
---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 128 +++-----------------
 1 file changed, 17 insertions(+), 111 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index dc03383c0..65600858f 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -4,32 +4,23 @@ Description : Proving goals under assumptions
 Copyright   : (c) Galois, Inc 2024
 License     : BSD3
 
-== Overview
-
-The functions in this module dispatch proof obligations arising from symbolic
-execution using SMT solvers. There are several dimensions of configurability,
-encapsulated in a 'ProofStrategy':
+This module contains helpers to dispatch the proof obligations arising from
+symbolic execution using SMT solvers. There are several dimensions of
+configurability, encapsulated in a 'ProofStrategy':
 
 * Offline vs. online: Offline solvers ('offlineProver') are simpler to manage
-  and more easily parallelized, but starting processes adds overhead; online
+  and more easily parallelized, but starting processes adds overhead, and online
   solvers ('onlineProver') can share state as assumptions are added. See the
   top-level README for What4 for further discussion of this choice.
 * Failing fast ('failFast') vs. keeping going ('keepGoing')
 * Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without
   ('offlineProve')
+* Parallelism: Not yet available via helpers in this module, but may be added to
+  a 'ProofStrategy' by clients.
 
 Once an appropriate strategy has been selected, it can be passed to entrypoints
 such as 'proveObligations' to dispatch proof obligations.
 
-== Parallelism
-
-Parallel proving is available via a separate set of entrypoints, e.g,
-'proveGoalsInParallel'. It only makes sense to use these with offline 'Prover's.
-Furthermore, these can only be used with 'ProofStrategy's that operate in the
-'IO' monad.
-
-== Proving goals
-
 When proving a single goal, the overall approach is:
 
 * Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
@@ -79,10 +70,6 @@ module Lang.Crucible.Backend.Prove
   , proveGoals
   , proveObligations
   , proveCurrentObligations
-    -- * Proving goals in parallel
-  , proveGoalsInParallel
-  , proveObligationsInParallel
-  , proveCurrentObligationsInParallel
   ) where
 
 import qualified Control.Concurrent as CC
@@ -90,7 +77,6 @@ import qualified Control.Concurrent.Async as CCA
 import qualified Control.Concurrent.QSem as CCQ
 import qualified Control.Exception as X
 import           Control.Lens ((^.))
-import           Control.Monad (foldM)
 import           Control.Monad.Catch (MonadMask)
 import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
@@ -143,15 +129,14 @@ consumeGoalsWithAssumptions onGoal onConj goals =
       (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
       (\g1 g2 -> onConj <$> g1 <*> g2)
 
--- | Not exported, but see 'proveGoalsInParallel'
 consumeGoalsParallel ::
   Monoid asmp =>
   -- | Consume a 'Prove'
-  (asmp -> goal -> IO r) ->
+  (asmp -> goal -> IO a) ->
   -- | Consume a 'ProveConj'
-  (r -> r -> IO r) ->
+  (IO () -> IO () -> IO ()) ->
   CB.Goals asmp goal ->
-  IO r
+  IO [a]
 consumeGoalsParallel onGoal onConj goals = do
   caps <- CC.getNumCapabilities
   sem <- liftIO $ CCQ.newQSem caps
@@ -161,48 +146,8 @@ consumeGoalsParallel onGoal onConj goals = do
         task' <- CCA.async (withQSem (onGoal asmps goal))
         IORef.modifyIORef' workers (task':)
         pure ()
-  consumeGoalsWithAssumptions onGoal' (>>) goals
-  go onConj =<< IORef.readIORef workers
-  where
-    go :: (r -> r -> IO r) -> [CCA.Async r] -> IO r
-    go combine tasks =
-      partitionPoll tasks >>=
-        \case
-          ([], []) -> error "Impossible"
-          ([], rest) -> delay >> go combine rest
-          ((r:rs), rest) -> do
-            accum <- foldM combine r rs
-            foldMReady combine accum rest
-  
-    -- Pause for 0.1 s = 1 * 10^5 microsecs
-    delay = do
-      let pointOneSecond = 100000
-      CC.threadDelay pointOneSecond
-
-    -- Like foldl', but processes the inputs whenever they're ready, rather than
-    -- in the order in which they're supplied in the list. Polls repeatedly, but
-    -- with a delay.
-    foldMReady :: (b -> a -> IO b) -> b -> [CCA.Async a] -> IO b
-    foldMReady f accum as = do
-      (ready, rest) <- partitionPoll as
-      result <- foldM f accum ready
-      if null rest
-      then pure result
-      else do
-        delay
-        foldMReady f result rest
-
-    -- Partition a list of tasks into those that are ready (in which case,
-    -- extract their results), and those that are still in progress.
-    partitionPoll :: [CCA.Async r] -> IO ([r], [CCA.Async r])
-    partitionPoll [] = pure ([], [])
-    partitionPoll (x:xs) = do
-      (ready, waiting) <- partitionPoll xs
-      CCA.poll x >>=
-        \case
-          Just (Left exn) -> X.throwIO exn
-          Just (Right r) -> pure (r:ready, waiting)
-          Nothing -> pure (ready, x:waiting)
+  consumeGoalsWithAssumptions onGoal' onConj goals
+  mapM CCA.wait =<< IORef.readIORef workers
 
 ---------------------------------------------------------------------
 -- * Strategy
@@ -514,56 +459,17 @@ proveCurrentObligations bak strat k = do
   proveObligations strat obligations k
 
 ---------------------------------------------------------------------
--- * Proving goals in parallel
+-- * Parallelism
 
--- | Prove a collection of 'CB.Goals' using the specified offline
--- 'ProofStrategy'.
---
--- TODO: details!
 proveGoalsInParallel ::
   Semigroup r =>
-  -- | Strategy with offline prover (e.g., 'offlineProver')
   ProofStrategy sym IO t r ->
-  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
   ProofConsumer sym t r ->
-  IO r
-proveGoalsInParallel strat goals k =
-  subgoalResult <$>
+  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
+  IO [r]
+proveGoalsInParallel strat k goals =
+  map subgoalResult <$>
     consumeGoalsParallel
       (\asmps gl -> proverProve (stratProver strat) asmps gl k)
-      (\r1 r2 -> getCombiner (stratCombine strat) (pure r1) (pure r2))
+      (>>)
       goals
-
--- | Prove a collection of 'CB.ProofObligations' in parallel using an offline
--- 'ProofStrategy'.
---
--- For more details, see 'proveGoalsInParallel'.
-proveObligationsInParallel ::
-  Monoid r =>
-  -- | Strategy with offline prover (e.g., 'offlineProver')
-  ProofStrategy sym IO t r ->
-  CB.ProofObligations sym ->
-  ProofConsumer sym t r ->
-  IO r
-proveObligationsInParallel strat obligations k =
-  case obligations of
-    Nothing -> pure mempty
-    Just goals -> proveGoalsInParallel strat goals k
-
--- | Prove a the current collection of 'CB.ProofObligations' associated with the
--- symbolic backend (retrieved via 'CB.getProofObligations') in parallel using
--- an offline 'ProofStrategy'.
---
--- For more details, see 'proveGoalsInParallel'.
-proveCurrentObligationsInParallel ::
-  Monoid r =>
-  (sym ~ WE.ExprBuilder t st fs) =>
-  CB.IsSymBackend sym bak =>
-  bak ->
-  -- | Strategy with offline prover (e.g., 'offlineProver')
-  ProofStrategy sym IO t r ->
-  ProofConsumer sym t r ->
-  IO r
-proveCurrentObligationsInParallel bak strat k = do
-  obligations <- liftIO (CB.getProofObligations bak)
-  proveObligationsInParallel strat obligations k

From ef8f5fba3bc3f5a44c23282e23edfa3470dff3d9 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 1 Jul 2024 16:14:43 -0400
Subject: [PATCH 13/16] Revert "Proving goals in parallel"

This reverts commit a836bc3cafcbc26bb3a87d365c3b23a8fb59dcae.
---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 42 +--------------------
 1 file changed, 1 insertion(+), 41 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 65600858f..a63a34136 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -46,6 +46,7 @@ assertion)@.
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Lang.Crucible.Backend.Prove
   ( -- * Strategy
@@ -72,16 +73,11 @@ module Lang.Crucible.Backend.Prove
   , proveCurrentObligations
   ) where
 
-import qualified Control.Concurrent as CC
-import qualified Control.Concurrent.Async as CCA
-import qualified Control.Concurrent.QSem as CCQ
-import qualified Control.Exception as X
 import           Control.Lens ((^.))
 import           Control.Monad.Catch (MonadMask)
 import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
 import qualified Control.Monad.Reader as Reader
-import qualified Data.IORef as IORef
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
@@ -129,26 +125,6 @@ consumeGoalsWithAssumptions onGoal onConj goals =
       (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
       (\g1 g2 -> onConj <$> g1 <*> g2)
 
-consumeGoalsParallel ::
-  Monoid asmp =>
-  -- | Consume a 'Prove'
-  (asmp -> goal -> IO a) ->
-  -- | Consume a 'ProveConj'
-  (IO () -> IO () -> IO ()) ->
-  CB.Goals asmp goal ->
-  IO [a]
-consumeGoalsParallel onGoal onConj goals = do
-  caps <- CC.getNumCapabilities
-  sem <- liftIO $ CCQ.newQSem caps
-  workers <- liftIO $ IORef.newIORef []
-  let onGoal' asmps goal = do
-        let withQSem = X.bracket_ (CCQ.waitQSem sem) (CCQ.signalQSem sem) 
-        task' <- CCA.async (withQSem (onGoal asmps goal))
-        IORef.modifyIORef' workers (task':)
-        pure ()
-  consumeGoalsWithAssumptions onGoal' onConj goals
-  mapM CCA.wait =<< IORef.readIORef workers
-
 ---------------------------------------------------------------------
 -- * Strategy
 
@@ -457,19 +433,3 @@ proveCurrentObligations ::
 proveCurrentObligations bak strat k = do
   obligations <- liftIO (CB.getProofObligations bak)
   proveObligations strat obligations k
-
----------------------------------------------------------------------
--- * Parallelism
-
-proveGoalsInParallel ::
-  Semigroup r =>
-  ProofStrategy sym IO t r ->
-  ProofConsumer sym t r ->
-  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
-  IO [r]
-proveGoalsInParallel strat k goals =
-  map subgoalResult <$>
-    consumeGoalsParallel
-      (\asmps gl -> proverProve (stratProver strat) asmps gl k)
-      (>>)
-      goals

From dfd4170e19f43358a40a656ac6f2a46c6c81f910 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 1 Jul 2024 16:16:54 -0400
Subject: [PATCH 14/16] Add a type annotation to a local helper

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index a63a34136..977d35b85 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -109,6 +109,7 @@ consumeGoals onAssumption onGoal onConj = go
 
 -- | Local helper
 consumeGoalsWithAssumptions ::
+  forall asmp goal a.
   Monoid asmp =>
   -- | Consume a 'Prove'
   (asmp -> goal -> a) ->
@@ -119,6 +120,7 @@ consumeGoalsWithAssumptions ::
 consumeGoalsWithAssumptions onGoal onConj goals =
   Reader.runReader (go goals) mempty
   where
+  go :: CB.Goals asmp goal -> Reader.Reader asmp a
   go =
     consumeGoals
       (\asmp gl -> Reader.local (<> asmp) gl)

From 442289e27b5646e04d2b5437eb9446610ca71cf1 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 1 Jul 2024 16:20:58 -0400
Subject: [PATCH 15/16] Haddocks for goal-proving helpers

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 977d35b85..0f8caefbd 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -133,6 +133,9 @@ consumeGoalsWithAssumptions onGoal onConj goals =
 -- | The result of attempting to prove a goal with an SMT solver.
 --
 -- The constructors of this type correspond to those of 'W4R.SatResult'.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @r@ is the return type of the eventual 'ProofConsumer'
 data ProofResult sym t
    = -- | The goal was proved.
      --
@@ -143,6 +146,9 @@ data ProofResult sym t
      -- The 'WE.GroundEvalFn' is only available for use during the execution of
      -- a 'ProofConsumer'. See 'WSA.SolverAdapter'.
      --
+     -- The @'Maybe' 'WE.ExprRangeBindings'@ are 'Just' when using
+     -- 'offlineProve' and 'Nothing' when using 'onlineProve'.
+     --
      -- Corresponds to 'W4R.Sat'.
    | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
      -- | The SMT solver returned \"unknown\".
@@ -151,6 +157,11 @@ data ProofResult sym t
    | Unknown
 
 -- | A 'ProofStrategy' dictates how results are proved.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
+-- * @t@ is the parameter to 'WE.Expr'
+-- * @r@ is the return type of the eventual 'ProofConsumer'
 data ProofStrategy sym m t r
   = ProofStrategy
     { -- | Generally 'offlineProver' or 'onlineProver'
@@ -162,6 +173,9 @@ data ProofStrategy sym m t r
 --
 -- If the result is 'Disproved', then this function must consume the
 -- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @t@ is the parameter to 'WE.Expr'
 newtype ProofConsumer sym t r
   = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)
 
@@ -178,6 +192,9 @@ data SubgoalResult r
   deriving Functor
 
 -- | How to combine results of proofs, used as part of a 'ProofStrategy'.
+--
+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
+-- * @r@ is the return type of the eventual 'ProofConsumer'
 newtype Combiner m r
   = Combiner
     { getCombiner ::

From f6814fb8982ce86fa1a5f15c484eeac3a297bb0f Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 2 Jul 2024 10:34:06 -0400
Subject: [PATCH 16/16] More haddocks for goal-proving helpers

---
 crucible/src/Lang/Crucible/Backend/Prove.hs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
index 0f8caefbd..5e8193f3a 100644
--- a/crucible/src/Lang/Crucible/Backend/Prove.hs
+++ b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -135,7 +135,7 @@ consumeGoalsWithAssumptions onGoal onConj goals =
 -- The constructors of this type correspond to those of 'W4R.SatResult'.
 --
 -- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
--- * @r@ is the return type of the eventual 'ProofConsumer'
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
 data ProofResult sym t
    = -- | The goal was proved.
      --
@@ -160,7 +160,7 @@ data ProofResult sym t
 --
 -- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
 -- * @m@ is the monad in which the 'Prover' and 'Combiner' run
--- * @t@ is the parameter to 'WE.Expr'
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
 -- * @r@ is the return type of the eventual 'ProofConsumer'
 data ProofStrategy sym m t r
   = ProofStrategy
@@ -175,7 +175,8 @@ data ProofStrategy sym m t r
 -- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.
 --
 -- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
--- * @t@ is the parameter to 'WE.Expr'
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
+-- * @r@ is the return type of the callback
 newtype ProofConsumer sym t r
   = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)