diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Release history for copilot-verifier
+
+## 0.1 (February 2024)
+
+* Initial release of `copilot-verifier.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2021-2024 Galois Inc.
+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 Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 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,327 @@
+# Copilot Verifier
+
+This "Copilot Verifier" is an add-on to the
+[Copilot Stream DSL](https://copilot-language.github.io)
+for verifying the correctness of C code generated
+by the `copilot-c99` package.
+
+The main idea of the verifier is to use the
+[Crucible symbolic simulator](https://github.com/galoisinc/crucible)
+to interpret the semantics of the generated C program and
+and to produce verification conditions sufficient to guarantee
+that the meaning of the generated program corresponds in a precise
+way to the meaning of the original stream specification. The generated
+verification conditions are then dispatched to SMT solvers to
+be automatically solved.  We will have more to say about exactly
+what is meant by this correspondence below.
+
+## Building
+
+To build the verifier from source, first make sure you have met the following
+prerequisites:
+
+* Ensure that you have the `cabal` and `ghc` executables in your `PATH`. If you
+  don't already have them, we recommend using `ghcup` to install them:
+  https://www.haskell.org/ghcup/. We recommend `Cabal` 3.10 or newer, and one of
+  GHC 8.10, 9.2, or 9.4.
+
+* Ensure that you have the `clang` and `llvm-link` utilities from LLVM in your
+  `PATH`. Currently, LLVM versions up to 16 are supported. LLVM binaries are
+  available at https://github.com/llvm/llvm-project/releases.
+
+* Ensure that you have the `z3` SMT solver in your `PATH`. `z3` binaries are
+  available at https://github.com/Z3Prover/z3/releases.
+
+Then, clone the repo and run:
+
+```
+$ git submodule update --init
+$ cabal test copilot-verifier
+```
+
+This will clone the repository, build the verifier, and run the associated test
+suite. If you have performed all of the steps above correctly, the test suite
+should pass.
+
+## Using the Copilot Verifier
+
+The main interface to the verifier is the `Copilot.Verifier.verify`
+function, which takes some options to drive the code generation
+process and a Copilot `Spec` object. It will invoke the Copilot
+code generator to obtain C sources, compile the C sources into
+LLVM bitcode using the `clang` compiler front-end, then
+parse and interpret the bitcode using `crucible`.  After generating
+verification conditions, it will dispatch them to an SMT solver,
+and the result of those queries will be presented to the user.
+
+There are a number of examples (based on similar examples
+from the main Copilot repository) demonstrating how to
+incorporate the verifier into a Copilot program.
+See the `copilot-verifier/examples` subdirectory of this repository.
+
+## Details of the Verification
+
+### Synopsis of Copilot semantics
+
+The Copilot DSL represents a certain nicely-behaved
+class of discrete-time stream programs. Each `Stream`
+in Copilot denotes an infinite stream of values; one may
+just as well think that `Stream a` represents a pure mathematical
+function `ℕ → a` from natural numbers to values of type `a`.
+See the
+[Copilot manual](https://ntrs.nasa.gov/api/citations/20200003164/downloads/20200003164.pdf)
+for more details of the Copilot language itself and its semantics.
+
+One of the central design considerations for Copilot is that is should
+be possible to implement stream programs using a fixed, finite amount
+of storage.  As a result, Copilot will only accept stream programs
+that access a bounded amount of their input streams (including any
+recursive stream references). This allows an
+implementation strategy where the generated C code can use fixed-size
+ring buffers to store a limited number of previous stream values.
+
+The execution model for the generated programs is that the program
+starts in a state corresponding to stream values at time `t = 0`;
+"external" stream input values are placed in distinguished global
+variables by the calling environment, which then executes a `step()`
+function to move to the next time step.  The `step()` function captures
+the values of these external inputs and does whatever computation is
+necessary to update its internal state from time `t=n` to time
+`t=n+1`.  In addition, it will call any defined "trigger" functions
+if the stream state at that time step satisfies the defined guard condition.
+In short, the generated C program steps one moment at a time through
+the stream program, consuming a sequence of input values provided by
+a cooperating environment and calling handler functions whenever
+states of interest occur.
+
+### The Desired Correspondence
+
+What does it mean, then, for a generated C program in this style
+to correctly implement a given stream program? The intuition
+is basically that after `n` calls to the `step` function,
+the state of the ring-buffers of the C program should correctly
+compute the value of the corresponding stream expression
+evaluated at index `n`, assuming the C program has been fed
+inputs corresponding to the first `n` values of the external stream
+inputs.  Moreover, the trigger functions should be called from
+the `step` function exactly at the time values when the stream expressions
+evaluate to true.
+
+The notion of correspondence for the values flowing in streams is
+relatively straightforward: these values consist of fixed-width
+machine integers, floating-point values, structs and fixed-length
+arrays. For each, the appropriate notion of equality is fairly clear.
+
+Both the original `Stream` program and the generated C program
+can be viewed straightforwardly as a transition system, and under
+this view, the correspondence we want to establish is a bisimulation
+between the states of the high-level stream program and the low-level
+C program. The proof method for bisimulation requires us to provide
+a "correspondence" relation between the program states, and then prove
+three things about this relation:
+
+1. that the initial states of the programs are in the relation;
+2. if we assume two arbitrary program states begin in the relation
+and each takes a single transition (consuming corresponding inputs),
+the resulting states are back in the relation;
+3. that any observable
+actions taken by one program are exactly mirrored by the other.
+
+On the high-level side of the bisimulation, the program
+state is essentially just the value of the current time step `n`,
+whereas on the C side it consists of the regions of global memory that
+contain the ring-buffers and their current indices.  The transition
+relation for the high-level program just increments the time value by
+one, and the transition for the C program is defined by the action
+of the generated `step()` function.
+
+Suppose `s` is one of the stream definitions in the original Copilot
+program which is required to retain `k` previous values;
+let `buf` be the global variable name of the ring-buffer in the C
+program, and `idx` be the global variable name maintaining the
+current index into the ring buffer.  Then the correspondence
+relation is basically that `0 <= idx < k` and
+`s[n+i] = buf[(idx+i) mod k]` as `i` ranges from `0 .. k-1`.
+By abuse of notation, here we mean that `s[j]` is
+the value of the stream expression `s` evaluated at index `j`,
+whereas `buf[j]` means the value obtained by reading the `j`th value
+of the buffer `buf` from memory.  The overall correspondence relation
+is a conjunction of statements like this, one for each stream
+expression that is realized via a buffer.
+
+### Implementing the Bisimulation proof steps
+
+The kind of program correspondence property we desire is a largely
+mechanical affair. As the code under consideration is automatically
+generated, it has a very regular structure and is specifically
+intended to implement the semantics we wich to verify it against.  As
+such, we expect these proofs to be highly automatable.
+
+The proof principle of bisimulation itself is not amenable
+to reduction to SMT, as if falls outside the first-order theories
+those solvers understand. Likewise, the semantics of Copilot
+and C might possibly be reducible directly to SMT, but it would be
+impractical to do so. However, we can reduce the individual
+proof obligations mentioned above into a series of lower-level
+logical statements that are amenable to SMT proof by
+defining the logical semantics of stream programs, and using
+symbolic simulation techniques to interpret the semantics of the
+C program.  Performing this reduction is the key contribution
+of `copilot-verifier`.
+
+#### Initial state correspondence
+
+The proof first obligation we must discharge is to show that
+the initial states of the two programs correspond. For each
+stream `s` there is a corresponding `k`, which is the length of
+the ring-buffer implementing it.  We must simply verify that
+the C program initializes its buffer with the first `k` values
+of the stream `s`, and that the `idx` value starts at 0.
+Because of the restrictions Copilot places on programs, these
+first `k` values must be specified concretely and will not be
+able to depend on any external inputs.  As such, this step
+is quite easily performed, as it requires only direct evaluation
+of concrete inputs.
+
+#### Transition correspondence
+
+The bulk of the proof effort consists of demonstrating that
+the bisimulation relation is preserved by transitions.
+In order to do this step, we must begin with totally symbolic
+initial states: we know nothing except that we are at some
+arbitrary time value `n`, and that the C program buffers
+correspond to their stream values as required by the relation.
+Thus, we create fresh symbolic variables for the streams
+from `n` to `n + k-1`, and for the values of all the involved
+external streams at time `n`. Then, we run forward the Copilot
+program by evaluating the stream recurrence expression to
+compute the value of each stream at time `n+k`.
+
+Next we set up an initial state of the C program by choosing,
+for each ring buffer, an arbitrary value for its current index
+within its allowed range, and then writing the variables
+corresponding to each stream value into the buffers at
+their appropriate offsets. The symbolic simulator is then
+invoked to compute the state update effects of the `step()`
+function. Afterward, we read the poststate values from the
+ring-buffers and verify that they correspond to the stream
+values from `n+1` up to `n+k`.
+
+As part of symbolic simulation, Crucible may also generate
+side-conditions that relate to memory safety of the program, or to
+error conditions that must be avoided. All of the bisimulation
+equivalence conditions and the safety side-conditions will be
+submitted to an SMT solver.
+
+#### Observable effects
+
+For our purposes, the only observable effects of a Copilot program
+relate to any "trigger" functions defined in the spec.  Our task is to
+show that the generated C code calls the external trigger functions if
+and only if the corresponding guard condition is true, and that the
+arguments passed to those functions are as expected.
+This proof obligation is proved in the same phase along with
+the transition relation proof above because the `step()` function
+is responsible for both invoking triggers and for performing state
+updates.
+
+The technique we use to perform this aspect of the proof is to
+install "override" functions to the external symbols corresponding
+to the C trigger functions before we begin symbolic simulation.
+In a real system, the external environment would be responsible
+for implementing these functions and taking whatever appropriate
+action is necessary when the triggers fire. However, we are verifying
+the generated code in isolation from its environment, so we have no
+implementation in hand. Instead, the override will
+essentially implement a stub function that simply captures its
+arguments and the path condition under which it was called.
+After simulation completes, the captured arguments and path condition
+are required to be equivalent to the corresponding trigger guard
+and arguments from the Copilot spec.  These conditions are
+discharged to the SMT solver at the same time as the transition
+relation obligations.
+
+Because of the way we model the trigger functions, we make a number of
+implicit assumptions about how the actual implementations of those
+functions must behave. The most important of those assumptions is that
+the trigger functions must not modify any memory under the control of
+the Copilot program, including its ring buffers and stack.  We also
+assume that the trigger functions are well defined, i.e. they are
+memory safe and do not perform any undefined behavior.
+
+#### Partial operations
+
+A generated C program may make use of partial operations. These range from
+division, which can fail if the second argument is zero, to signed integer
+arithmetic, which can overflow and result in undefined behavior. The verifier
+has two modes for dealing with partial operations:
+
+1. Any invocation of a partial operation on undefined inputs in the generated
+   C program will result in an error, provided that the user did not add an
+   assertion that assumes this behavior will not occur.
+
+2. If the generated C program invokes a partial operation on undefined inputs,
+   the verifier will check if this coincides with a corresponding invocation
+   of a partial operation in the Copilot spec. If so, the verification will
+   succeed. In other words, the verifier will check that the spec and the
+   C program are "crash-equivalent".
+
+The verifier uses mode (1) by default, but mode (2) can be enabled by using
+`Copilot.Verifier.verifyWithOptions sideCondVerifierOptions`. In this mode,
+the verifier will analyze any invocation of a operation which could be partial
+and generate a side condition that this operation will only be invoked on
+well defined inputs. During the transition step of the bisimulation proof,
+the verifier will add these side conditions as assumptions. Therefore, if
+simulating the C program generates any side conditions due to invoking partial
+operations, these side conditions from the C program should be dischargeable
+using the corresponding side conditions from the Copilot spec.
+
+Mode (2) has the caveat that `clang` may compile C code to LLVM bitcode in
+which a partial function is no longer applied to undefined inputs. For
+instance, `clang` will sometimes promote 16-bit integer values to 32 bits
+before performing arithmetic on them. This can turn an operation that would
+result in signed 16-bit integer overflow into a 32-bit integer operation
+that does _not_ overflow, for instance.
+
+### Caveats About the Verifier
+
+We rely on the `clang` compiler front-end to consume C source files
+and produce LLVM intermediate language, which then becomes the input
+to the later verification steps. To the extent that the input program
+is not fully-portable C, `clang` may make implementation-specific
+decisions about how to compile the program which might be made
+different if compiled by a different compiler (e.g. `gcc`). We expect
+this aspect to be mitigated by the fact that Copilot programs are
+automatically generated into a rather simple subset of the C language,
+and is designed to be as simple as possible.
+Any code-generation bugs in `clang` itself may affect the soundness
+of our verifier. Again, however, Copilot generates a well-understood
+subset of the language, and we expect `clang` to be well-tested on
+the code patterns produced.
+
+The semantics of LLVM bitcode, as encoded in the `crucible-llvm`
+package, may have errors that affect soundness. We mitigate this risk
+by testing our semantics against a corpus of verification problems
+produced for the SV-COMP verification competition, paying special
+attention to any soundness issues that arise. `Crux`, a standalone
+verification system based on `crucible-llvm`, was a participant in the
+2022 edition of SV-COMP.
+
+The semantics of Copilot programs, as encoded in the
+`Copilot.Theorem.What4` module may have errors that affect soundness.
+For the moment we do not have an effective mitigation strategy for
+this risk other than manual examination and comparison against the
+intended semantics of Copilot, as encoded in the interpreter.
+
+There is limited SMT solver support for floating-point values,
+especially for transcendental functions like the trig primitives.  As a
+result, we reason about floating point expressions via uninterpreted
+functions. In other words, we leave the semantics of the
+floating-point operations totally abstract, and simply verify that the
+Copilot program and the corresponding C program apply the same
+operations in the same order. This is sound, but leaves the possibility
+that the compiler will apply some correct transformation to
+floating-point expressions that we are nonetheless unable to verify.
+However, on low optimizations and without the `--fast-math` flag,
+compilers generally (and `clang` in particular) are very reluctant to
+rearrange floating-point code, and the verifications generally succeed.
diff --git a/copilot-verifier.cabal b/copilot-verifier.cabal
new file mode 100644
--- /dev/null
+++ b/copilot-verifier.cabal
@@ -0,0 +1,146 @@
+Cabal-version: 2.2
+Name:          copilot-verifier
+Version:       0.1
+Author:        Galois Inc.
+Maintainer:    rscott@galois.com
+Copyright:     (c) Galois, Inc 2021-2024
+License:       BSD-3-Clause
+License-file:  LICENSE
+Build-type:    Simple
+Category:      Language
+Synopsis:      System for verifying the correctness of generated Copilot programs
+Description:
+  @copilot-verifier@ is an add-on to the <https://copilot-language.github.io
+  Copilot Stream DSL> for verifying the correctness of C code generated by the
+  @copilot-c99@ package.
+  .
+  @copilot-verifier@ uses the <https://github.com/galoisinc/crucible Crucible
+  symbolic simulator> to interpret the semantics of the generated C program and
+  and to produce verification conditions sufficient to guarantee that the
+  meaning of the generated program corresponds in a precise way to the meaning
+  of the original stream specification. The generated verification conditions
+  are then dispatched to SMT solvers to be automatically solved.
+extra-doc-files: CHANGELOG.md, README.md
+
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/copilot-verifier
+  subdir:   copilot-verifier
+
+common bldflags
+  ghc-options: -Wall
+               -Werror=incomplete-patterns
+               -Werror=missing-methods
+               -Werror=overlapping-patterns
+               -Wpartial-fields
+               -Wincomplete-uni-patterns
+  ghc-prof-options: -O2 -fprof-auto-exported
+  default-language: Haskell2010
+  default-extensions:
+     NondecreasingIndentation
+  build-depends:
+    aeson >= 1.5 && < 2.3,
+    base >= 4.8 && < 4.18,
+    bv-sized >= 1.0.0 && < 1.1,
+    bytestring,
+    containers >= 0.5.9.0,
+    copilot >= 3.18.1 && < 3.19,
+    copilot-c99 >= 3.18.1 && < 3.19,
+    copilot-core >= 3.18.1 && < 3.19,
+    copilot-libraries >= 3.18.1 && < 3.19,
+    copilot-language >= 3.18.1 && < 3.19,
+    copilot-prettyprinter >= 3.18.1 && < 3.19,
+    copilot-theorem >= 3.18.1 && < 3.19,
+    crucible >= 0.7 && < 0.8,
+    crucible-llvm >= 0.6 && < 0.7,
+    crux >= 0.7 && < 0.8,
+    crux-llvm >= 0.8 && < 0.9,
+    filepath,
+    lens,
+    llvm-pretty,
+    mtl,
+    panic >= 0.3,
+    parameterized-utils >= 2.1.4 && < 2.2,
+    prettyprinter >= 1.7.0,
+    text,
+    transformers,
+    vector,
+    what4 >= 0.4
+
+library
+  import: bldflags
+
+  hs-source-dirs: src
+  exposed-modules:
+    Copilot.Verifier
+    Copilot.Verifier.Log
+
+library copilot-verifier-examples
+  import: bldflags
+
+  hs-source-dirs: examples
+  build-depends:
+    case-insensitive,
+    copilot-verifier
+  exposed-modules:
+    Copilot.Verifier.Examples
+
+    Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
+    Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
+    Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
+    Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
+    Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
+    Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
+    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
+    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
+    Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
+
+    Copilot.Verifier.Examples.ShouldPass.Array
+    Copilot.Verifier.Examples.ShouldPass.ArrayGen
+    Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
+    Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
+    Copilot.Verifier.Examples.ShouldPass.Arith
+    Copilot.Verifier.Examples.ShouldPass.Clock
+    Copilot.Verifier.Examples.ShouldPass.Counter
+    Copilot.Verifier.Examples.ShouldPass.Engine
+    Copilot.Verifier.Examples.ShouldPass.FPOps
+    Copilot.Verifier.Examples.ShouldPass.Heater
+    Copilot.Verifier.Examples.ShouldPass.IntOps
+    Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
+    Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
+    Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
+    Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
+    Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
+    Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
+    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
+    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
+    Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
+    Copilot.Verifier.Examples.ShouldPass.Structs
+    Copilot.Verifier.Examples.ShouldPass.Voting
+    Copilot.Verifier.Examples.ShouldPass.WCV
+
+executable verify-examples
+  import: bldflags
+
+  hs-source-dirs: exe
+  main-is: VerifyExamples.hs
+  build-depends:
+    case-insensitive,
+    copilot-verifier,
+    copilot-verifier-examples,
+    optparse-applicative
+
+test-suite copilot-verifier-test
+  import: bldflags
+
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  build-depends:
+    case-insensitive,
+    copilot-verifier,
+    copilot-verifier-examples,
+    silently >= 1.2,
+    tasty >= 0.10,
+    tasty-expected-failure >= 0.12,
+    tasty-hunit >= 0.10
+  main-is: Test.hs
diff --git a/examples/Copilot/Verifier/Examples.hs b/examples/Copilot/Verifier/Examples.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Copilot.Verifier.Examples
+  ( shouldFailExamples
+  , shouldPassExamples
+  ) where
+
+import qualified Data.CaseInsensitive as CI
+import Data.CaseInsensitive (CI)
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.Text (Text)
+
+import Copilot.Verifier (Verbosity)
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin        as Fail.AbsIntMin
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap    as Fail.AddSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero        as Fail.DivByZero
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds as Fail.IndexOutOfBounds
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero        as Fail.ModByZero
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap    as Fail.MulSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge   as Fail.ShiftLTooLarge
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge   as Fail.ShiftRTooLarge
+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap    as Fail.SubSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldPass.Array                    as Array
+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayGen                 as ArrayGen
+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs           as ArrayOfStructs
+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument     as ArrayTriggerArgument
+import qualified Copilot.Verifier.Examples.ShouldPass.Arith                    as Arith
+import qualified Copilot.Verifier.Examples.ShouldPass.Clock                    as Clock
+import qualified Copilot.Verifier.Examples.ShouldPass.Counter                  as Counter
+import qualified Copilot.Verifier.Examples.ShouldPass.Engine                   as Engine
+import qualified Copilot.Verifier.Examples.ShouldPass.FPOps                    as FPOps
+import qualified Copilot.Verifier.Examples.ShouldPass.Heater                   as Heater
+import qualified Copilot.Verifier.Examples.ShouldPass.IntOps                   as IntOps
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin        as Pass.AbsIntMin
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap    as Pass.AddSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds as Pass.IndexOutOfBounds
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero        as Pass.DivByZero
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero        as Pass.ModByZero
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap    as Pass.MulSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge   as Pass.ShiftLTooLarge
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   as Pass.ShiftRTooLarge
+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap    as Pass.SubSignedWrap
+import qualified Copilot.Verifier.Examples.ShouldPass.Structs                  as Structs
+import qualified Copilot.Verifier.Examples.ShouldPass.Voting                   as Voting
+import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV
+
+shouldFailExamples :: Verbosity -> Map (CI Text) (IO ())
+shouldFailExamples verb = Map.fromList
+    [ -- Partial operation tests
+      example "AbsIntMin-fail" (Fail.AbsIntMin.verifySpec verb)
+    , example "AddSignedWrap-fail" (Fail.AddSignedWrap.verifySpec verb)
+    , example "DivByZero-fail" (Fail.DivByZero.verifySpec verb)
+    , example "IndexOutOfBounds-fail" (Fail.IndexOutOfBounds.verifySpec verb)
+    , example "ModByZero-fail" (Fail.ModByZero.verifySpec verb)
+    , example "MulSignedWrap-fail" (Fail.MulSignedWrap.verifySpec verb)
+    , example "ShiftLTooLarge-fail" (Fail.ShiftLTooLarge.verifySpec verb)
+    , example "ShiftRTooLarge-fail" (Fail.ShiftRTooLarge.verifySpec verb)
+    , example "SubSignedWrap-fail" (Fail.SubSignedWrap.verifySpec verb)
+    ]
+
+shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())
+shouldPassExamples verb = Map.fromList
+    [ example "Array" (Array.verifySpec verb)
+    , example "ArrayGen" (ArrayGen.verifySpec verb)
+    , example "ArrayOfStructs" (ArrayOfStructs.verifySpec verb)
+    , example "ArrayTriggerArgument" (ArrayTriggerArgument.verifySpec verb)
+    , example "Arith" (Arith.verifySpec verb)
+    , example "Clock" (Clock.verifySpec verb)
+    , example "Counter" (Counter.verifySpec verb)
+    , example "Engine" (Engine.verifySpec verb)
+    , example "FPOps" (FPOps.verifySpec verb)
+    , example "Heater" (Heater.verifySpec verb)
+    , example "IntOps" (IntOps.verifySpec verb)
+    , example "Structs" (Structs.verifySpec verb)
+    , example "Voting" (Voting.verifySpec verb)
+    , example "WCV" (WCV.verifySpec verb)
+
+      -- Partial operation tests
+    , example "AbsIntMin-pass" (Pass.AbsIntMin.verifySpec verb)
+    , example "AddSignedWrap-pass" (Pass.AddSignedWrap.verifySpec verb)
+    , example "DivByZero-pass" (Pass.DivByZero.verifySpec verb)
+    , example "IndexOutOfBounds-pass" (Pass.IndexOutOfBounds.verifySpec verb)
+    , example "ModByZero-pass" (Pass.ModByZero.verifySpec verb)
+    , example "MulSignedWrap-pass" (Pass.MulSignedWrap.verifySpec verb)
+    , example "ShiftLTooLarge-pass" (Pass.ShiftLTooLarge.verifySpec verb)
+    , example "ShiftRTooLarge-pass" (Pass.ShiftRTooLarge.verifySpec verb)
+    , example "SubSignedWrap-pass" (Pass.SubSignedWrap.verifySpec verb)
+    ]
+
+example :: Text -> IO () -> (CI Text, IO ())
+example name action = (CI.mk name, action)
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @notIntMin@ property, which is needed to prevent undefined behavior when
+-- invoking the 'abs' function.
+module Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int32
+      stream = extern "stream" Nothing
+
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
+  trigger "streamAbs" (abs stream == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["notIntMin"]
+    []
+    "absIntMinFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @notIntMax@ property, which is needed to prevent signed integer overflow.
+module Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int32
+      stream = extern "stream" Nothing
+
+  _ <- prop "notIntMax" (forAll (stream < constI32 maxBound))
+  trigger "streamAddSigned" ((stream + 1) == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["notIntMax"]
+    []
+    "addSignedWrapFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @nonzero@ property, which is needed to prevent a division-by-zero error.
+module Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int16
+      stream = extern "stream" Nothing
+
+  _ <- prop "nonzero" (forAll (stream /= 0))
+  trigger "streamDiv" ((stream `div` stream) == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["nonzero"]
+    []
+    "divByZeroFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @withinBounds@ property, which is needed to prevent an out-of-bounds array index.
+module Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream1 :: Stream (Array 2 Int16)
+      stream1 = constant (array [27, 42])
+
+      stream2 :: Stream Word32
+      stream2 = extern "stream2" Nothing
+
+  _ <- prop "withinBounds" (forAll (stream2 < constW32 2))
+  trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["withinBounds"]
+    []
+    "indexFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @nonzero@ property, which is needed to prevent a division-by-zero error.
+module Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int16
+      stream = extern "stream" Nothing
+
+  _ <- prop "nonzero" (forAll (stream /= 0))
+  trigger "streamMod" ((stream `mod` stream) == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["nonzero"]
+    []
+    "modByZeroFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @withinRange@ property, which is needed to prevent signed integer underflow or overflow.
+module Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap where
+
+import qualified Prelude as P
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int32
+      stream = extern "stream" Nothing
+
+  _ <- prop "withinRange" (forAll
+           (constI32 ((minBound P.+ 1) P.* 2) < stream
+         && stream < constI32 ((maxBound P.- 1) `P.div` 2)))
+  trigger "streamMulSigned" ((stream * 2) == 2) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["withinRange"]
+    []
+    "mulSignedWrapFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @lessThanBitWidth@ property, which is needed to prevent shifting by too
+-- large of a value.
+module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream1 :: Stream Int32
+      stream1 = extern "stream1" Nothing
+
+      stream2 :: Stream Int64
+      stream2 = extern "stream2" Nothing
+
+  _ <- prop "lessThanBitWidth" (forAll
+         (constI64 0 <= stream2 && stream2 < constI64 32))
+  trigger "streamShiftL" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["lessThanBitWidth"]
+    []
+    "shiftLTooLargeFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @lessThanBitWidth@ property, which is needed to prevent shifting by too
+-- large of a value.
+module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream1 :: Stream Int32
+      stream1 = extern "stream1" Nothing
+
+      stream2 :: Stream Int64
+      stream2 = extern "stream2" Nothing
+
+  _ <- prop "lessThanBitWidth" (forAll
+         (constI64 0 <= stream2 && stream2 < constI64 32))
+  trigger "streamShiftR" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["lessThanBitWidth"]
+    []
+    "shiftRTooLargeFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @notIntMin@ property, which is needed to prevent signed integer underflow.
+module Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int32
+      stream = extern "stream" Nothing
+
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
+  trigger "streamSubSigned" ((stream - 1) == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    -- ["notIntMin"]
+    []
+    "subSignedWrapFail" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
@@ -0,0 +1,52 @@
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Verifier.Examples.ShouldPass.Arith where
+
+import Control.Monad (when)
+import qualified Prelude as P
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Copilot.Theorem.What4 (prove, Solver(..))
+
+-- The largest unsigned 32-bit prime
+lastPrime :: Stream Word32
+lastPrime = 31
+--lastPrime = 4294967291 -- Whelp, this prime seems too big for the solvers to handle well
+
+multRingSpec :: Spec
+multRingSpec = do
+  _ <- prop "clamp nonzero" (forAll ((clamp > 0) && (clamp < lastPrime)))
+  _ <- prop "reduced" (forAll (acc < lastPrime))
+  _ <- prop "nonzero" (forAll (acc > 0 && (acc < lastPrime)))
+
+  trigger "outofrange" (not (acc > 0 && acc < lastPrime)) [arg acc]
+
+  return ()
+
+  where
+  -- a stream of external values
+  vals  = externW32 "values" Nothing
+
+  -- Generate a value in [1, lastPrime), which
+  -- is the multiplictive group of Z_p
+  clamp :: Stream Word32
+  clamp = (vals `mod` (lastPrime - 1)) + 1
+
+  -- Successively multiply new values
+  acc :: Stream Word32
+  acc = [1] ++ unsafeCast ((cast acc * cast clamp) `mod` (cast lastPrime :: Stream Word64))
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb =
+  do s <- reify multRingSpec
+     r <- prove Z3 s
+     when (verb P.>= Default) $
+       print r
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings ["reduced"] "multRingSpec" s
+
+--verifySpec _ = interpret 10 engineMonitor
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs
@@ -0,0 +1,40 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | This is a simple example for arrays. As a program, it does not make much
+-- sense, however it shows of the features of arrays nicely.
+
+-- | Enable compiler extension for type-level data, necesary for the array
+-- length.
+
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+module Copilot.Verifier.Examples.ShouldPass.Array where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+-- Lets define an array of length 2.
+-- Make the buffer of the streams 3 elements long.
+arr :: Stream (Array 2 Bool)
+arr = [ array [True, False]
+      , array [True, True]
+      , array [False, False]] ++ arr
+
+spec :: Spec
+spec = do
+  -- A trigger that fires 'func' when the first element of 'arr' is True.
+  -- It passes the current value of arr as an argument.
+  -- The prototype of 'func' would be:
+  -- void func (int8_t arg[3]);
+  trigger "func" (arr .!! 0) [arg arr]
+
+-- Compile the spec
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "array"
+-- verifySpec _ = interpret 30 spec
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+module Copilot.Verifier.Examples.ShouldPass.ArrayGen where
+
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Language.Copilot
+import qualified Prelude hiding ((++), (>))
+
+spec :: Spec
+spec = trigger "f" (stream .!! 0 > 0) [arg stream]
+  where
+    stream :: Stream (Array 2 Int16)
+    stream = [array [3,4]] ++ rest
+
+    rest :: Stream (Array 2 Int16)
+    rest = constant $ array [5,6]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "arrayGen"
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs where
+
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Language.Copilot
+
+data S = S { field :: Field "field" Int16 }
+
+instance Struct S where
+  typename _ = "s"
+  toValues s = [Value Int16 (field s)]
+
+instance Typed S where
+  typeOf = Struct (S (Field 0))
+
+spec :: Spec
+spec = trigger "f" ((stream .!! 0)#field == 27) [arg stream]
+  where
+    stream :: Stream (Array 2 S)
+    stream = [array [S (Field 27), S (Field 42)]] ++ stream
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "arrayOfStructs" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+
+-- | A regression test for
+-- <https://github.com/Copilot-Language/copilot/issues/431>.
+module Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = trigger "f" true [arg stream]
+  where
+    stream :: Stream (Array 2 Int16)
+    stream = constant (array [3,4])
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions
+    defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings [] "arrayTriggerArgument" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
@@ -0,0 +1,46 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Example showing usage of clocks to generate periodically recurring truth
+-- values.
+
+module Copilot.Verifier.Examples.ShouldPass.Clock where
+
+import Control.Monad (when)
+import qualified Prelude as P
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Copilot.Theorem.What4 (prove, Solver(..))
+
+-- | We need to force a type for the argument of `period`.
+p :: Word8
+p = 5
+
+-- | Both have the same period, but a different phase.
+clkStream :: Stream Bool
+clkStream  = clk (period p) (phase 0)
+
+clkStream' :: Stream Bool
+clkStream' = clk (period p) (phase 2)
+
+spec :: Spec
+spec = do
+  observer "clk"  clkStream
+  observer "clk'" clkStream'
+  _ <- prop "clksPhase" (forAll (clkStream == drop 2 clkStream'))
+  _ <- prop "clksDistinct" (forAll (not (clkStream && clkStream')))
+  trigger "clksHigh" (clkStream && clkStream') []
+
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb =
+  do s <- reify spec
+     r <- prove Z3 s
+     when (verb P.>= Default) $
+       print r
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings [] "clock" s
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
@@ -0,0 +1,56 @@
+-------------------------------------------------------------------------------
+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Example showing an implementation of a resettable counter.
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Verifier.Examples.ShouldPass.Counter where
+
+import Control.Monad (when)
+import qualified Prelude as P
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Copilot.Theorem.What4 (prove, Solver(..))
+
+-- A resettable counter
+counter :: (Typed a, Integral a) => Stream Bool -> Stream Bool -> Stream a
+counter inc reset = cnt
+  where
+    cnt = if reset then 0
+          else if inc then z + 1
+               else z
+    z = [0] ++ cnt
+
+-- Counter that resets when it reaches 256
+bytecounter :: Stream Int32
+bytecounter = counter true (resetcounter `mod` 256 == 0)
+
+resetcounter :: Stream Word32
+resetcounter = counter true false
+
+bytecounter2 :: Stream Int32
+bytecounter2 = counter true ([False] ++ bytecounter2 == 255)
+
+spec :: Spec
+spec =
+  do _ <- prop "range" (forAll (bytecounter == unsafeCast (resetcounter `mod` 256)))
+     _ <- prop "range2" (forAll (0 <= bytecounter2 && bytecounter2 <= 255))
+     _ <- prop "same"  (forAll ((0 <= bytecounter2 && bytecounter2 <= 255) &&
+                                (bytecounter == unsafeCast (resetcounter `mod` 256)) &&
+                                (bytecounter == bytecounter2)))
+     trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]
+
+verifySpec :: Verbosity -> IO ()
+-- verifSpec _ = interpret 1280 spec
+verifySpec verb =
+  do s <- reify spec
+     r <- prove Z3 s
+     when (verb P.>= Default) $
+       print r
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings ["range", "range2"] "counter" s
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs
@@ -0,0 +1,44 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Example implementing an engine cooling control system.
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Verifier.Examples.ShouldPass.Engine where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+import qualified Prelude as P
+
+{- If the majority of the engine temperature probes exeeds 250 degrees, then
+ - the cooler is engaged and remains engaged until the majority of the engine
+ - temperature probes drop to 250 or below.  Otherwise, trigger an immediate
+ - shutdown of the engine.
+-}
+
+engineMonitor :: Spec
+engineMonitor = do
+  trigger "shutoff" (not ok) [arg maj]
+
+  where
+  vals     = [ externW8 "tmp_probe_0" two51
+             , externW8 "tmp_probe_1" two51
+             , externW8 "tmp_probe_2" zero]
+  exceed   = map (> 250) vals
+  maj      = majority exceed
+  checkMaj = aMajority exceed maj
+  ok       = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler)
+
+  two51  = Just $ [251, 251] P.++ repeat (250 :: Word8)
+  zero   = Just $ repeat (0 :: Word8)
+  cooler = Just $ [True, True] P.++ repeat False
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify engineMonitor >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                            mkDefaultCSettings [] "engine"
+--verifySpec _ = interpret 10 engineMonitor
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs b/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module Copilot.Verifier.Examples.ShouldPass.FPOps where
+
+import Copilot.Compile.C99 (mkDefaultCSettings)
+import qualified Copilot.Language.Stream as Copilot
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Data.Proxy (Proxy(..))
+import Language.Copilot
+import qualified Prelude as P
+
+mkSpecFor :: forall a proxy. (RealFloat a, Typed a) => proxy a -> String -> Spec
+mkSpecFor _ nameSuffix = do
+  let mkName :: String -> String
+      mkName namePrefix = namePrefix P.++ nameSuffix
+
+      stream :: Stream a
+      stream = extern (mkName "stream") Nothing
+
+  triggerOp1 (mkName "abs") abs stream
+  triggerOp1 (mkName "signum") signum stream
+  triggerOp1 (mkName "recip") recip stream
+  triggerOp1 (mkName "exp") exp stream
+  triggerOp1 (mkName "sqrt") sqrt stream
+  triggerOp1 (mkName "log") log stream
+  triggerOp1 (mkName "sin") sin stream
+  triggerOp1 (mkName "tan") tan stream
+  triggerOp1 (mkName "cos") cos stream
+  triggerOp1 (mkName "asin") asin stream
+  triggerOp1 (mkName "atan") atan stream
+  triggerOp1 (mkName "acos") acos stream
+  triggerOp1 (mkName "sinh") sinh stream
+  triggerOp1 (mkName "tanh") tanh stream
+  triggerOp1 (mkName "cosh") cosh stream
+  triggerOp1 (mkName "asinh") asinh stream
+  triggerOp1 (mkName "atanh") atanh stream
+  triggerOp1 (mkName "acosh") acosh stream
+  triggerOp1 (mkName "ceiling") Copilot.ceiling stream
+  triggerOp1 (mkName "floor") Copilot.floor stream
+
+  triggerOp2 (mkName "add") (+) stream
+  triggerOp2 (mkName "sub") (-) stream
+  triggerOp2 (mkName "mul") (*) stream
+  triggerOp2 (mkName "div") (/) stream
+  triggerOp2 (mkName "pow") (**) stream
+  triggerOp2 (mkName "logBase") logBase stream
+  triggerOp2 (mkName "atan2") Copilot.atan2 stream
+
+spec :: Spec
+spec = do
+  mkSpecFor (Proxy @Float) "F"
+  mkSpecFor (Proxy @Double) "D"
+
+triggerOp1 :: (RealFloat a, Typed a) =>
+              String ->
+              (Stream a -> Stream a) ->
+              Stream a ->
+              Spec
+triggerOp1 name op stream =
+  trigger (name P.++ "Trigger") (testOp1 op stream) [arg stream]
+
+triggerOp2 :: (RealFloat a, Typed a) =>
+              String ->
+              (Stream a -> Stream a -> Stream a) ->
+              Stream a ->
+              Spec
+triggerOp2 name op stream =
+  trigger (name P.++ "Trigger") (testOp2 op stream) [arg stream]
+
+testOp1 :: (RealFloat a, Typed a) =>
+           (Stream a -> Stream a) -> Stream a -> Stream Bool
+testOp1 op stream =
+  -- NB: Use (>=) rather than (==) here, as floating-point equality gets weird
+  -- due to NaNs.
+  op stream >= op stream
+
+testOp2 :: (RealFloat a, Typed a) =>
+           (Stream a -> Stream a -> Stream a) -> Stream a -> Stream Bool
+testOp2 op stream =
+  op stream stream >= op stream stream
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "fpOps" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs
@@ -0,0 +1,60 @@
+--------------------------------------------------------------------------------
+-- Copyright 2019 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- This is a simple example with basic usage. It implements a simple home
+-- heating system: It heats when temp gets too low, and stops when it is high
+-- enough. It read temperature as a byte (range -50C to 100C) and translates
+-- this to Celcius.
+
+module Copilot.Verifier.Examples.ShouldPass.Heater where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.PrettyPrint as PP
+--import Copilot.Language.Prelude
+
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+import qualified Prelude as P
+import Control.Monad (when)
+
+-- External temperature as a byte, range of -50C to 100C
+temp :: Stream Word8
+temp = extern "temperature" Nothing
+
+-- Calculate temperature in Celcius.
+-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
+-- is no direct relation between Word8 and Float.
+ctemp :: Stream Float
+ctemp = (unsafeCast temp * constant (150.0/255.0)) - constant 50.0
+
+-- width of the sliding window
+window :: Int
+window = 5
+
+-- Compute the sliding average of the last 5 temps
+-- (Here, 19.5 is the average of 18.0 and 21.0, the two temperature extremes
+-- that we check for in the spec.)
+avgTemp :: Stream Float
+avgTemp = (sum window (replicate window 19.5 ++ ctemp)) / fromIntegral window
+
+spec :: Spec
+spec = do
+  trigger "heaton"  (avgTemp < 18.0) [arg avgTemp]
+  trigger "heatoff" (avgTemp > 21.0) [arg avgTemp]
+
+-- Compile the spec
+verifySpec :: Verbosity -> IO ()
+verifySpec verb =
+  do rspec <- reify spec
+     when (verb P.>= Default) $ putStrLn (PP.prettyPrint rspec)
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings [] "heater"
+                       rspec
+
+{-
+  do spec' <- reify spec
+     putStrLn $ prettyPrintDot spec'
+-}
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs b/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module Copilot.Verifier.Examples.ShouldPass.IntOps where
+
+import Copilot.Compile.C99 (mkDefaultCSettings)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+import Language.Copilot
+import qualified Prelude as P
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int16
+      stream = extern "stream" Nothing
+
+      shiftBy :: Stream Int16
+      shiftBy = extern "shiftBy" Nothing
+
+  _ <- prop "nonzero" (forAll (stream /= 0))
+  _ <- prop "shiftByBits" (forAll (0 <= shiftBy && shiftBy < 16))
+
+  triggerOp1 "abs" abs stream
+  triggerOp1 "signum" signum stream
+  triggerOp1 "bwNot" complement stream
+
+  triggerOp2 "add" (+) stream stream
+  triggerOp2 "sub" (-) stream stream
+  triggerOp2 "mul" (*) stream stream
+  triggerOp2 "mod" mod stream stream
+  triggerOp2 "div" div stream stream
+  triggerOp2 "bwAnd" (.&.) stream stream
+  triggerOp2 "bwOr" (.|.) stream stream
+  triggerOp2 "bwXor" (.^.) stream stream
+  triggerOp2 "bwShiftL" (.<<.) stream shiftBy
+  triggerOp2 "bwShiftR" (.>>.) stream shiftBy
+
+triggerOp1 :: String ->
+              (Stream Int16 -> Stream Int16) ->
+              Stream Int16 ->
+              Spec
+triggerOp1 name op stream =
+  trigger (name P.++ "Trigger") (testOp1 op stream) [arg stream]
+
+triggerOp2 :: String ->
+              (Stream Int16 -> Stream Int16 -> Stream Int16) ->
+              Stream Int16 -> Stream Int16 ->
+              Spec
+triggerOp2 name op stream1 stream2 =
+  trigger (name P.++ "Trigger") (testOp2 op stream1 stream2) [arg stream1, arg stream2]
+
+testOp1 :: (Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool
+testOp1 op stream =
+  op stream == op stream
+
+testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16) ->
+           Stream Int16 -> Stream Int16 ->
+           Stream Bool
+testOp2 op stream1 stream2 =
+  op stream1 stream2 == op stream1 stream2
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AbsIntMin.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AbsIntMin.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AbsIntMin.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Abs@
+-- operation is well defined precisely when C's @abs@ function is well defined.
+module Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "absIntMinPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AddSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AddSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/AddSignedWrap.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Add@
+-- operation should overflow on signed integers precisely when C addition does.
+module Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "addSignedWrapPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/DivByZero.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/DivByZero.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/DivByZero.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Div@
+-- operation is well defined precisely when C division is well defined.
+module Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "divByZeroPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/IndexOutOfBounds.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/IndexOutOfBounds.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/IndexOutOfBounds.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's indexing
+-- operation should be out of bounds precisely when C array indexes are out of bounds.
+module Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "indexPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ModByZero.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ModByZero.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ModByZero.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Mod@
+-- operation is well defined precisely when C's @%@ operator is well defined.
+module Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "modByZeroPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/MulSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/MulSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/MulSignedWrap.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Mul@
+-- operation should wrap on signed integers precisely when C multiplication does.
+module Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "mulSignedWrapPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftLTooLarge.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftLTooLarge.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftLTooLarge.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @BwShiftL@
+-- operation should only accept second arguments as large as C's @<<@ operation does.
+module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "shiftLTooLargePass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftRTooLarge.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftRTooLarge.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftRTooLarge.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @BwShiftR@
+-- operation should only accept second arguments as large as C's @>>@ operation does.
+module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "shiftRTooLargePass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Partial/SubSignedWrap.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/SubSignedWrap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Partial/SubSignedWrap.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Sub@
+-- operation should underflow on signed integers precisely when C subtraction does.
+module Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , sideCondVerifierOptions, verifyWithOptions )
+import Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap (spec)
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
+    []
+    "subSignedWrapPass" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
@@ -0,0 +1,92 @@
+-- | An example showing the usage of the What4 backend in copilot-theorem for
+-- structs and arrays. Particular focus is on nested structs.
+-- For general usage of structs, refer to the general structs example.
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module Copilot.Verifier.Examples.ShouldPass.Structs where
+
+import Control.Monad (void, forM_, when)
+import qualified Prelude as P
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Theorem.What4
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+
+-- | Definition for `Volts`.
+data Volts = Volts
+  { numVolts :: Field "numVolts" Word16
+  , flag     :: Field "flag"     Bool
+  }
+
+-- | `Struct` instance for `Volts`.
+instance Struct Volts where
+  typename _ = "volts"
+  toValues vlts = [ Value Word16 (numVolts vlts)
+                  , Value Bool   (flag vlts)
+                  ]
+
+-- | `Volts` instance for `Typed`.
+instance Typed Volts where
+  typeOf = Struct (Volts (Field 0) (Field False))
+
+data Battery = Battery
+  { temp  :: Field "temp"  Word16
+  , volts :: Field "volts" (Array 10 Volts)
+  , other :: Field "other" (Array 10 (Array 5 Word32))
+  }
+
+-- | `Battery` instance for `Struct`.
+instance Struct Battery where
+  typename _ = "battery"
+  toValues battery = [ Value typeOf (temp battery)
+                     , Value typeOf (volts battery)
+                     , Value typeOf (other battery)
+                     ]
+
+-- | `Battery` instance for `Typed`. Note that `undefined` is used as an
+-- argument to `Field`. This argument is never used, so `undefined` will never
+-- throw an error.
+instance Typed Battery where
+  typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))
+
+spec :: Spec
+spec = do
+  let battery :: Stream Battery
+      battery = extern "battery" Nothing
+
+  -- Check equality, indexing into nested structs and arrays. Note that this is
+  -- trivial by equality.
+  void $ prop "Example 1" $ forAll $
+    (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)
+
+  -- Same as previous example, but get a different array index (so should be
+  -- false).
+  void $ prop "Example 2" $ forAll $
+    (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
+
+  -- Same as previous example, but in trigger form
+  trigger "otherTrig" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))
+                      [arg battery]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+
+  -- Use Z3 to prove the properties.
+  results <- prove Z3 spec'
+
+  -- Print the results.
+  when (verb P.>= Default) $
+    forM_ results $ \(nm, res) -> do
+      putStr $ nm <> ": "
+      case res of
+        Valid   -> putStrLn "valid"
+        Invalid -> putStrLn "invalid"
+        Unknown -> putStrLn "unknown"
+
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "structs" spec'
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs
@@ -0,0 +1,64 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Fault-tolerant voting examples.
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Verifier.Examples.ShouldPass.Voting where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+vote :: Spec
+vote = do
+  -- majority selects element with the biggest occurance.
+  trigger "maj"  true [arg maj]
+
+  -- aMajority checks if the selected element has a majority.
+  trigger "aMaj" true [arg $ aMajority inputs maj]
+
+  where
+    maj = majority inputs
+
+    -- 26 input streams to vote on
+    inputs :: [Stream Word32]
+    inputs = [ a, b, c, d, e, f, g, h, i, j, k, l, m
+             -- , n, o, p, q, r, s, t, u, v, w, x, y, z
+             ]
+    a = [0] ++ a + 1
+    b = [0] ++ b + 1
+    c = [0] ++ c + 1
+    d = [0] ++ d + 1
+    e = [1] ++ e + 1
+    f = [1] ++ f + 1
+    g = [1] ++ g + 1
+    h = [1] ++ h + 1
+    i = [1] ++ i + 1
+    j = [1] ++ j + 1
+    k = [1] ++ k + 1
+    l = [1] ++ l + 1
+    m = [1] ++ m + 1
+{-
+    n = [1] ++ n + 1
+    o = [1] ++ o + 1
+    p = [1] ++ p + 1
+    q = [1] ++ q + 1
+    r = [1] ++ r + 1
+    s = [1] ++ s + 1
+    t = [1] ++ t + 1
+    u = [1] ++ u + 1
+    v = [1] ++ v + 1
+    w = [1] ++ w + 1
+    x = [1] ++ x + 1
+    y = [1] ++ y + 1
+    z = [1] ++ z + 1
+-}
+
+verifySpec :: Verbosity -> IO ()
+--verifySpec _ = interpret 30 vote
+verifySpec verb = reify vote >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "voting"
diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
new file mode 100644
--- /dev/null
+++ b/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
@@ -0,0 +1,194 @@
+-- | This example shows an implementation of the Well-Clear Violation
+-- algorithm, it follows the implementation described in 'Analysis of
+-- Well-Clear Bounday Models for the Integration of UAS in the NAS',
+-- https://ntrs.nasa.gov/citations/20140010078.
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Verifier.Examples.ShouldPass.WCV where
+
+import Language.Copilot
+import qualified Copilot.Theorem.What4 as CT
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+import qualified Prelude as P
+import Data.Foldable (forM_)
+import qualified Control.Monad as Monad
+
+
+-- | `dthr` is the horizontal distance threshold.
+dthr :: Stream Double
+dthr = extern "dthr" Nothing
+
+-- | `tthr` is the horizontal time threshold.
+tthr :: Stream Double
+tthr = extern "tthr" Nothing
+
+-- | `zthr` is the vertical distance / altitude threshold.
+zthr :: Stream Double
+zthr = extern "zthr" Nothing
+
+-- | `tcoathr` is the vertical time threshold.
+tcoathr :: Stream Double
+tcoathr = extern "tcoathr" Nothing
+
+type Vect2 = (Stream Double, Stream Double)
+
+
+--------------------------------
+-- External streams for relative position and velocity.
+--------------------------------
+
+-- | The relative x velocity between ownship and the intruder.
+vx :: Stream Double
+vx = extern "relative_velocity_x" Nothing
+
+-- | The relative y velocity between ownship and the intruder.
+vy :: Stream Double
+vy = extern "relative_velocity_y" Nothing
+
+-- | The relative z velocity between ownship and the intruder.
+vz :: Stream Double
+vz = extern "relative_velocity_z" Nothing
+
+-- | The relative velocity as a 2D vector.
+v :: (Stream Double, Stream Double)
+v = (vx, vy)
+
+
+-- | The relative x position between ownship and the intruder.
+sx :: Stream Double
+sx = extern "relative_position_x" Nothing
+
+-- | The relative y position between ownship and the intruder.
+sy :: Stream Double
+sy = extern "relative_position_y" Nothing
+
+-- | The relative z position between ownship and the intruder.
+sz :: Stream Double
+sz = extern "relative_position_z" Nothing
+
+-- | The relative position as a 2D vector.
+s :: (Stream Double, Stream Double)
+s = (sx, sy)
+
+
+------------------
+-- The following section contains basic libraries for working with vectors.
+------------------
+
+-- | Multiply two Vectors.
+(|*|) :: Vect2 -> Vect2 -> Stream Double
+(|*|) (x1, y1) (x2, y2) = (x1 * x2) + (y1 * y2)
+
+-- | Calculate the square of a vector.
+sq :: Vect2 -> Stream Double
+sq x = x |*| x
+
+-- | Calculate the length of a vector.
+norm :: Vect2 -> Stream Double
+norm = sqrt . sq
+
+-- | Calculate the determinant of two vectors.
+det :: Vect2 -> Vect2 -> Stream Double
+det (x1, y1) (x2, y2) = (x1 * y2) - (x2 * y1)
+
+-- | Compare two vectors, taking into account the small error that is
+-- introduced by the usage of `Double`s.
+(~=) :: Stream Double -> Stream Double -> Stream Bool
+a ~= b = (abs (a - b)) < 0.001
+
+-- | Negate a vector.
+neg :: Vect2 -> Vect2
+neg (x, y) = (negate x, negate y)
+
+
+--------------------
+-- From here on the algorithm, as described by the paper mentioned on the top
+-- of this file, is implemented. Please refer to the paper for details.
+--------------------
+
+tau :: Vect2 -> Vect2 -> Stream Double
+tau s v = if s |*| v < 0
+            then (-(sq s)) / (s |*| v)
+            else -1
+
+tcpa :: Vect2 -> Vect2 -> Stream Double
+tcpa s v@(vx, vy) = if vx ~= 0 && vy ~= 0
+                      then 0
+                      else -(s |*| v)/(sq v)
+
+taumod :: Vect2 -> Vect2 -> Stream Double
+taumod s v = if s |*| v < 0
+               then (dthr * dthr - (sq s))/(s |*| v)
+               else -1
+
+tep :: Vect2 -> Vect2 -> Stream Double
+tep s v = if (s |*| v < 0) && ((delta s v dthr) >= 0)
+            then theta s v dthr (-1)
+            else -1
+
+delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double
+delta s v d = (d*d) * (sq v) - ((det s v)*(det s v))
+-- Here the formula says : (s . orth v)^2 which is the same as det(s,v)^2
+
+theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double
+theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v)
+
+
+tcoa :: Stream Double -> Stream Double -> Stream Double
+tcoa sz vz = if (sz * vz) < 0
+               then (-sz) / vz
+               else -1
+
+dcpa :: Vect2 -> Vect2 -> Stream Double
+dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy)
+
+
+--------------------------
+-- Well clear Violation --
+--------------------------
+
+-- | Determines if the well clear property is violated or not.
+wcv :: (Vect2 -> Vect2 -> Stream Double) ->
+       Vect2 -> Stream Double ->
+       Vect2 -> Stream Double ->
+       Stream Bool
+wcv tvar s sz v vz = (horizontalWCV tvar s v) && (verticalWCV sz vz)
+
+verticalWCV :: Stream Double -> Stream Double -> Stream Bool
+verticalWCV sz vz =
+  ((abs $ sz) <= zthr) ||
+  (0 <= (tcoa sz vz) && (tcoa sz vz) <= tcoathr)
+
+horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool
+horizontalWCV tvar s v =
+  (norm s <= dthr) ||
+  (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
+
+spec = do
+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
+  -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
+  trigger "well_clear_violation" (wcv tep s sz v vz) []
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "wcv" spec'
+
+{-
+  -- Use Z3 to prove the properties.
+  results <- CT.prove CT.Z3 spec'
+
+  -- Print the results.
+  forM_ results $ \(nm, res) -> do
+    putStr $ nm <> ": "
+    case res of
+      CT.Valid -> putStrLn "valid"
+      CT.Invalid -> putStrLn "invalid"
+      CT.Unknown -> putStrLn "unknown"
+-}
diff --git a/exe/VerifyExamples.hs b/exe/VerifyExamples.hs
new file mode 100644
--- /dev/null
+++ b/exe/VerifyExamples.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Main (main) where
+
+import qualified Data.CaseInsensitive as CI
+import Data.CaseInsensitive (CI)
+import Data.Foldable (for_)
+import qualified Data.Map as Map
+import qualified Data.Text as Text
+import qualified Data.Text.IO as Text
+import Data.Text (Text)
+import Data.Traversable (for)
+import Options.Applicative
+
+import Copilot.Verifier (Verbosity(..))
+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)
+
+newtype Options = Options
+  { examples :: [CI Text]
+  } deriving Show
+
+optsParser :: Parser Options
+optsParser = Options
+  <$> (some . strArgument)
+      (  metavar "EXAMPLE1 [EXAMPLE2 ...]"
+      <> help "The names of the examples to run" )
+
+main :: IO ()
+main = execParser opts >>= verifyExamples
+  where
+    opts = info (optsParser <**> helper)
+      ( fullDesc
+     <> header "Run one or more copilot-verifier examples"
+     <> progDesc (unlines [ "Run one or more examples from the copilot-verifier/examples directory."
+                          , "Each EXAMPLE must correspond to an example name."
+                          ]))
+
+verifyExamples :: Options -> IO ()
+verifyExamples Options{examples} = do
+  -- Check that all requested examples exist
+  examplesWithMain <- for examples $ \example ->
+    case Map.lookup example (shouldFailExamples Default `Map.union` shouldPassExamples Default) of
+      Just m  -> pure (example, m)
+      Nothing -> fail $ "No example named " ++ Text.unpack (CI.original example)
+
+  -- Run the examples
+  for_ examplesWithMain $ \(example, exampleMain) -> do
+    Text.putStrLn "====="
+    Text.putStrLn $ "== Running the " <> CI.original example <> " example..."
+    Text.putStrLn "====="
+    Text.putStrLn ""
+    exampleMain
+    Text.putStrLn ""
diff --git a/src/Copilot/Verifier.hs b/src/Copilot/Verifier.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Verifier.hs
@@ -0,0 +1,1517 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Copilot.Verifier
+  ( verify
+  , verifyWithOptions
+  , VerifierOptions(..)
+  , defaultVerifierOptions
+  , sideCondVerifierOptions
+  , Verbosity(..)
+  ) where
+
+import Control.Lens (view, (^.), to)
+import Control.Monad (foldM, forM_, when)
+import Control.Monad.IO.Class (liftIO)
+import Control.Monad.State (execStateT, lift, StateT(..))
+import Data.Aeson (ToJSON)
+import Data.Foldable (traverse_)
+import Data.Functor (void)
+import qualified Data.Text as Text
+import qualified Data.Map.Strict as Map
+import Data.IORef (newIORef, modifyIORef', readIORef, IORef)
+import qualified Text.LLVM.AST as L
+import Data.List (genericLength)
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Vector as V
+import qualified Data.BitVector.Sized as BV
+import GHC.Generics (Generic)
+import qualified Prettyprinter as PP
+import System.Exit (exitFailure)
+import System.FilePath ((</>), (<.>))
+
+import Copilot.Compile.C99 (CSettings(..), compileWith)
+import Copilot.Core
+import qualified Copilot.Core.Type as CT
+
+import qualified Copilot.Theorem.What4 as CW4
+
+import qualified Copilot.Verifier.Log as Log
+
+import Data.Parameterized.Ctx (EmptyCtx)
+import Data.Parameterized.Context (pattern Empty)
+import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.NatRepr (intValue, natValue, testEquality, knownNat, type (<=) )
+import Data.Parameterized.Nonce (globalNonceGenerator)
+import Data.Parameterized.Some (Some(..))
+import Data.Parameterized.TraversableFC (toListFC)
+import Data.Parameterized.TraversableFC.WithIndex (ifoldlMFC)
+import qualified Data.Parameterized.Vector as PVec
+
+import Lang.Crucible.Backend
+  ( IsSymInterface, Goals(..), Assumptions, Assertion
+  , pushAssumptionFrame, popUntilAssumptionFrame
+  , getProofObligations, clearProofObligations
+  , LabeledPred(..), abortExecBecause, AbortExecReason(..), addAssumption
+  , addDurableProofObligation, assert, CrucibleAssumption(..), ppAbortExecReason
+  , IsSymBackend(..), HasSymInterface(..)
+  , labeledPred, labeledPredMsg
+  -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg
+  )
+import Lang.Crucible.Backend.Simple (newSimpleBackend)
+import Lang.Crucible.CFG.Core (AnyCFG(..), cfgArgTypes, cfgReturnType)
+import Lang.Crucible.CFG.Common ( freshGlobalVar )
+import Lang.Crucible.FunctionHandle (newHandleAllocator)
+import Lang.Crucible.Simulator
+  ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..)
+  , defaultAbortHandler, runOverrideSim, partialValue, gpValue
+  , GlobalVar, executeCrucible, OverrideSim, regValue
+  , readGlobal, modifyGlobal, callCFG, emptyRegMap, RegEntry(..)
+  , AbortedResult(..)
+  )
+import Lang.Crucible.Simulator.ExecutionTree ( withBackend )
+import Lang.Crucible.Simulator.GlobalState ( insertGlobal )
+import Lang.Crucible.Simulator.RegValue (RegValue, RegValue'(..))
+import Lang.Crucible.Simulator.SimError (SimError(..), SimErrorReason(..)) -- ppSimError
+import Lang.Crucible.Types
+  ( TypeRepr(..), (:~:)(..), KnownRepr(..), NatType )
+
+import Lang.Crucible.LLVM (llvmGlobals, registerLazyModule, register_llvm_overrides)
+import Lang.Crucible.LLVM.Bytes (bitsToBytes)
+import Lang.Crucible.LLVM.DataLayout (Alignment, DataLayout)
+import Lang.Crucible.LLVM.Errors (BadBehavior)
+import Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)
+import Lang.Crucible.LLVM.Globals (initializeAllMemory, populateAllGlobals)
+import Lang.Crucible.LLVM.Intrinsics
+  ( IntrinsicsOptions, OverrideTemplate, basic_llvm_override, LLVMOverride(..) )
+
+import Lang.Crucible.LLVM.MemType
+  ( MemType(..), SymType(..)
+  , i1, i8, i16, i32, i64
+  , memTypeSize, memTypeAlign
+  , mkStructInfo
+  )
+import Lang.Crucible.LLVM.MemModel
+  ( mkMemVar, withPtrWidth, HasLLVMAnn, LLVMAnnMap, MemImpl
+  , HasPtrWidth, doResolveGlobal, doStore
+  , LLVMPtr, LLVMVal, MemOptions, PartLLVMVal(..), StorageType, bitvectorType
+  , ptrAdd, toStorableType, projectLLVM_bv
+  , pattern LLVMPointerRepr, pattern PtrRepr, loadRaw, llvmPointer_bv
+  , memRepr, Mem, unpackMemValue
+  )
+import Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
+import Lang.Crucible.LLVM.MemModel.Partial (BoolAnn(..))
+import Lang.Crucible.LLVM.PrettyPrint (ppSymbol)
+import Lang.Crucible.LLVM.Translation
+  ( LLVMTranslationWarning(..), ModuleTranslation
+  , getTranslatedCFG, translateModule, globalInitMap
+  , transContext, llvmPtrWidth, llvmTypeCtx, llvmTypeAsRepr
+  )
+import Lang.Crucible.LLVM.TypeContext (TypeContext, llvmDataLayout)
+
+import Crux (defaultOutputConfig)
+import Crux.Config (cfgJoin, Config(..))
+import Crux.Config.Load (fromFile, fromEnv)
+import Crux.Config.Common
+  ( cruxOptions, CruxOptions(..), postprocessOptions, outputOptions
+  , OutputOptions(..)
+  )
+import Crux.Goal (proveGoalsOffline, provedGoalsTree)
+import qualified Crux.Log as Log
+import Crux.Types (SimCtxt, Crux, ProcessedGoals(..), ProofResult(..))
+
+import Crux.LLVM.Config (llvmCruxConfig, LLVMOptions(..))
+import Crux.LLVM.Compile (genBitCode)
+import qualified Crux.LLVM.Log as Log
+import Crux.LLVM.Simulate (setupSimCtxt, parseLLVM, explainFailure)
+import CruxLLVMMain (processLLVMOptions)
+
+import What4.Config
+  (extendConfig)
+import What4.Interface
+  ( Pred, bvLit, bvAdd, bvUrem, bvMul, bvIsNonzero, bvEq, isEq
+  , getConfiguration, freshBoundedBV, predToBV
+  , getCurrentProgramLoc, printSymExpr
+  , truePred, falsePred, andPred, annotateTerm, backendPred
+  , getAnnotation, natAdd, natEq, natIte, natLit
+  )
+import What4.Expr.Builder
+  ( FloatModeRepr(..), ExprBuilder, BoolExpr, startCaching
+  , newExprBuilder
+  )
+import What4.FunctionName (functionName)
+import What4.InterpretedFloatingPoint
+  ( FloatInfoRepr(..), IsInterpretedFloatExprBuilder(..)
+  , SingleFloat, DoubleFloat
+  )
+import What4.ProgramLoc (ProgramLoc, mkProgramLoc, plFunction, Position(..))
+import What4.Solver.Adapter (SolverAdapter(..))
+import What4.Solver.Z3 (z3Adapter)
+import What4.Symbol (safeSymbol)
+
+-- | @'verify' csettings props prefix spec@ verifies the Copilot specification
+-- @spec@ under the assumptions @props@ matches the behavior of the C program
+-- compiled with @csettings@ within a directory prefixed by @prefix@.
+verify :: CSettings -> [String] -> String -> Spec -> IO ()
+verify = verifyWithOptions defaultVerifierOptions
+
+-- | Options for configuring the behavior of the verifier.
+data VerifierOptions = VerifierOptions
+  { verbosity :: Verbosity
+    -- ^ How much output the verifier should produce.
+  , assumePartialSideConds :: Bool
+    -- ^ If 'True', the verifier will determine the conditions under which
+    --   a Copilot specification's partial operations are well defined and
+    --   add these side conditions as assumptions. As a result, even if the
+    --   generated C code performs a partial operation, the verification will
+    --   succeed if this partial operation coincides with a corresponding
+    --   operation on the Copilot side.
+    --
+    --   If 'False', the verifier will not assume any side conditions related
+    --   to partial operations in the Copilot specification. As a result, any
+    --   use of a partial operation in the generated C code will cause
+    --   verification to fail unless the user adds their own assumptions.
+  , logSmtInteractions :: Bool
+    -- ^ If 'True', create log files corresponding to the SMT solver
+    -- interactions used to discharge each proof goal. The file will be named
+    -- @<step>-<goal number>-<solver>.smt2@, where:
+    --
+    -- * @<step>@ will be either @initial-step@ or @transition-step@, depending
+    --   on which step of the proof the goal corresponds to.
+    --
+    -- * @<goal number>@ will be the number of the goal, starting at 0 and
+    --   counting up. Note that each step of the proof has its own goal
+    --   numbers. This means that there can be both an
+    --   @initial-step-0-<solver>.smt2@ and a @transition-step-0-<solver>.smt2@,
+    --   and similarly for other numbers.
+    --
+    -- * @<solver>@ is the name of the SMT solver used to discharge the proof
+    --   goal. Currently, this will always be @z3@, although we might make this
+    --   configurable in the future.
+  } deriving stock Show
+
+-- | The default 'VerifierOptions':
+--
+-- * Produce a reasonable amount of diagnostics as verification proceeds
+--   ('Default').
+--
+-- * Do not assume any side conditions related to partial operations.
+--
+-- * Do not log any SMT solver interactions.
+defaultVerifierOptions :: VerifierOptions
+defaultVerifierOptions = VerifierOptions
+  { verbosity = Default
+  , assumePartialSideConds = False
+  , logSmtInteractions = False
+  }
+
+-- | Like 'defaultVerifierOptions', except that the verifier will assume side
+-- conditions related to partial operations used in the Copilot spec.
+sideCondVerifierOptions :: VerifierOptions
+sideCondVerifierOptions = defaultVerifierOptions
+  { assumePartialSideConds = True
+  }
+
+-- | How much output should verification produce?
+--
+-- The data constructors are listed in increasing order of how many diagnostics
+-- they produce.
+data Verbosity
+  = Quiet   -- ^ Don't produce any diagnostics.
+  | Default -- ^ Produce a reasonable amount of diagnostics as verification proceeds.
+  | Noisy   -- ^ Produce as many diagnostics as possible.
+  deriving stock (Eq, Ord, Show)
+
+-- | Like 'verify', but with 'VerifierOptions' to more finely control the
+-- verifier's behavior.
+verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
+verifyWithOptions opts csettings0 properties prefix spec =
+  withCopilotLogging $
+  do -- munge options structures into the necessary forms
+     (ocfg, cruxOpts, llvmOpts, csettings, csrc) <- computeConfiguration opts csettings0 prefix
+     let ?outputConfig = ocfg
+
+     -- Compile the Copilot spec into C source code, using
+     -- preexisting Copilot library calls.
+     compileWith csettings prefix spec
+     Log.sayCopilot $ Log.GeneratedCFile csrc
+
+     -- Compile the C source into LLVM bitcode, using preexisting
+     -- Crux library calls.
+     bcFile <- genBitCode cruxOpts llvmOpts
+     Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile
+
+     -- Run the main verification procedure
+     verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile
+
+
+-- | Do the (surprisingly large amount) of options munging necessary to set up
+--   the crucible/crux environment.
+computeConfiguration ::
+  Log.SupportsCruxLogMessage CopilotLogging =>
+  VerifierOptions -> CSettings -> FilePath ->
+  IO (Log.OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings, FilePath)
+computeConfiguration opts csettings0 prefix =
+  do ocfg1 <- defaultOutputConfig copilotLoggingToSayWhat
+     let quiet = verbosity opts == Quiet
+     let ocfg2 mbOutputOpts = (ocfg1 mbOutputOpts) { Log._quiet = quiet }
+     llvmcfg <- llvmCruxConfig
+     let cfg = cfgJoin cruxOptions llvmcfg
+     -- TODO, load from an actual configuration file?
+     fileOpts <- fromFile "copilot-verifier" cfg Nothing
+     (cruxOpts0, llvmOpts0) <- foldM fromEnv fileOpts (cfgEnv cfg)
+     let odir0 = cSettingsOutputDirectory csettings0
+     let odir = -- A bit grimy, but this corresponds to how crux-llvm sets
+                -- its output directory.
+                if odir0 == "."
+                  then "results" </> prefix
+                  else odir0
+     let csettings = csettings0{ cSettingsOutputDirectory = odir }
+     let csrc = odir </> prefix ++ ".c"
+     let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc]
+                              , outputOptions =
+                                  (outputOptions cruxOpts0)
+                                    { quietMode = quiet
+                                    , simVerbose = if verbosity opts > Default
+                                                   then 2
+                                                   else 0
+                                    }
+                              }
+     let ?outputConfig = ocfg2 (Just (outputOptions cruxOpts1))
+     cruxOpts2 <- postprocessOptions cruxOpts1
+
+     -- Tweak the options passed to Clang:
+     --
+     -- - Fix the optimization level to -O0.
+     --
+     -- - Pass -ffp-contract=off to prevent sequences of floating-point
+     --   multiplications/additions from being optimized to llvm.fmuladd
+     --   intrinsics, which makes floating-point verification fragile.
+     let llvmOpts1 = llvmOpts0
+                       { optLevel = 0
+                       , clangOpts = "-ffp-contract=off" : clangOpts llvmOpts0
+                       }
+     (cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts1)
+
+     let ocfg3 = ocfg2 (Just (outputOptions cruxOpts3))
+     return (ocfg3, cruxOpts3, llvmOpts2, csettings, csrc)
+
+
+data CopilotVerifierData t = CopilotVerifierData
+
+
+-- | Main entry point for the verifier.
+verifyBitcode ::
+  Log.Logs msgs =>
+  Log.SupportsCruxLogMessage msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  VerifierOptions {- ^ Verifier-specific settings -} ->
+  CSettings   {- ^ Settings used to compile the Copilot spec. Used to find the names of functions and variables. -} ->
+  [String]    {- ^ Names of properties to assume during verification. -} ->
+  Spec        {- ^ The input Copilot specification -} ->
+  CruxOptions {- ^ Crux options -} ->
+  LLVMOptions {- ^ CruxLLVM options -} ->
+  FilePath    {- ^ Path to the bitcode file to verify -} ->
+  IO ()
+verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile =
+  do -- Set up the expression builder and symbolic backend
+     halloc <- newHandleAllocator
+     sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator
+     bak <- newSimpleBackend sym
+     -- turn on hash-consing
+     startCaching sym
+
+     -- capture LLVM side-condition information for use in error reporting
+     clRefs <- newCopilotLogRefs
+     let ?recordLLVMAnnotation = recordLLVMAnnotation clRefs
+
+     -- Set up the solver to use for verification.  Right now we hard-code this to Z3.
+     let adapters = [z3Adapter] -- TODO? configurable
+     extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym)
+
+     -- Set up the Crucible/LLVM simulation context
+     memVar <- mkMemVar "llvm_memory" halloc
+     let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
+                  { printHandle = view Log.outputHandle ?outputConfig }
+
+     -- Load and translate the input LLVM module
+     llvmMod <- parseLLVM bcFile
+     Some trans <-
+        let ?transOpts = transOpts llvmOpts
+         in translateModule halloc memVar llvmMod
+
+     Log.sayCopilot Log.TranslatedToCrucible
+
+     -- Grab some metadata from the bitcode file and options;
+     -- make the available via implicit arguments to the places
+     -- that expect them.
+     let llvmCtxt = trans ^. transContext
+     let ?lc = llvmCtxt ^. llvmTypeCtx
+     let ?memOpts = memOpts llvmOpts
+     let ?intrinsicsOpts = intrinsicsOpts llvmOpts
+
+     llvmPtrWidth llvmCtxt $ \ptrW ->
+       withPtrWidth ptrW $
+
+       do -- Compute the LLVM memory state with global variables allocated
+          -- but not initialized
+          emptyMem   <- initializeAllMemory bak llvmCtxt llvmMod
+
+          -- Compute the LLVM memory state with global variables initialized
+          -- to their initial values.
+          initialMem <- populateAllGlobals bak (trans ^. globalInitMap) emptyMem
+
+          -- Use the Copilot spec directly to compute the symbolic states
+          -- necessary to carry out the states of the bisimulation proof.
+          Log.sayCopilot Log.GeneratingProofState
+          proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec
+
+          -- First check that the initial state of the program matches the starting
+          -- segment of the associated Copilot streams.
+          let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts
+          verifyInitialState cruxOptsInit adapters clRefs simctx initialMem
+             (CW4.initialStreamState proofStateBundle)
+
+          -- Now, the real meat. Carry out the bisimulation step of the proof.
+          let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts
+          verifyStepBisimulation opts cruxOptsTrans adapters csettings
+             clRefs simctx llvmMod trans memVar initialMem proofStateBundle
+  where
+    -- If @logSmtInteractions@ is enabled, enable offline solver output in the
+    -- supplied 'CruxOptions' with the supplied file template. Otherwise, return
+    -- the supplied 'CruxOptions' unaltered.
+    setCruxOfflineSolverOutput :: FilePath -> CruxOptions -> CruxOptions
+    setCruxOfflineSolverOutput template cruxOpts'
+      | logSmtInteractions opts
+      = cruxOpts'
+          { offlineSolverOutput = Just $ outDir cruxOpts' </> template <.> "smt2" }
+      | otherwise
+      = cruxOpts'
+
+-- | Capture LLVM side-condition information for use in error reporting.
+recordLLVMAnnotation ::
+  IsSymInterface sym =>
+  CopilotLogRefs sym ->
+  CallStack ->
+  BoolAnn sym ->
+  BadBehavior sym ->
+  IO ()
+recordLLVMAnnotation clRefs stk bann bb =
+  modifyIORef' (llvmAnnMapRef clRefs) (Map.insert bann (stk, bb))
+
+-- | Prove that the state of the global variables at program startup
+--   matches the expected initial segments of the associated Copilot
+--   streams.
+verifyInitialState ::
+  IsSymInterface sym =>
+  Log.Logs msgs =>
+  Log.SupportsCruxLogMessage msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  sym ~ ExprBuilder t st fs =>
+  HasPtrWidth wptr =>
+  HasLLVMAnn sym =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+
+  CruxOptions ->
+  [SolverAdapter st] ->
+  CopilotLogRefs sym ->
+  SimCtxt Crux sym LLVM ->
+  MemImpl sym ->
+  CW4.BisimulationProofState sym ->
+  IO ()
+verifyInitialState cruxOpts adapters clRefs simctx mem initialState =
+  withBackend simctx $ \bak ->
+  do Log.sayCopilot $ Log.ComputingConditions Log.InitialState
+     frm <- pushAssumptionFrame bak
+
+     assertStateRelation bak clRefs mem initialState
+
+     popUntilAssumptionFrame bak frm
+
+     Log.sayCopilot $ Log.ProvingConditions Log.InitialState
+     proveObls cruxOpts adapters clRefs Log.InitialState simctx
+
+
+verifyStepBisimulation ::
+  IsSymInterface sym =>
+  Log.Logs msgs =>
+  Log.SupportsCruxLogMessage msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  sym ~ ExprBuilder t st fs =>
+  HasPtrWidth wptr =>
+  HasLLVMAnn sym =>
+  (1 <= ArchWidth arch) =>
+  HasPtrWidth (ArchWidth arch) =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+  (?intrinsicsOpts :: IntrinsicsOptions) =>
+
+  VerifierOptions ->
+  CruxOptions ->
+  [SolverAdapter st] ->
+  CSettings ->
+  CopilotLogRefs sym ->
+  SimCtxt Crux sym LLVM ->
+  L.Module ->
+  ModuleTranslation arch ->
+  GlobalVar Mem ->
+  MemImpl sym ->
+  CW4.BisimulationProofBundle sym ->
+  IO ()
+verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod modTrans memVar mem prfbundle =
+  withBackend simctx $ \bak ->
+  do Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation
+
+     frm <- pushAssumptionFrame bak
+
+     do -- set up the memory image
+        mem' <- setupPrestate bak mem prfbundle
+
+        -- sanity check, verify that we set up the memory in the expected relation
+        assertStateRelation bak clRefs mem' (CW4.preStreamState prfbundle)
+
+        -- set up trigger guard global variables
+        let halloc = simHandleAllocator simctx
+        -- See Note [Global variables for trigger functions]
+        let prepTrigger (nm, guard, _) =
+              do gv <- freshGlobalVar halloc (Text.pack (nm ++ "_called")) NatRepr
+                 return (nm, gv, guard)
+        triggerGlobals <- mapM prepTrigger (CW4.triggerState prfbundle)
+
+        -- execute the step function
+        let overrides = zipWith (triggerOverride clRefs) triggerGlobals (CW4.triggerState prfbundle)
+        mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)
+
+        -- assert the poststate is in the relation
+        assertStateRelation bak clRefs mem'' (CW4.postStreamState prfbundle)
+
+     popUntilAssumptionFrame bak frm
+
+     Log.sayCopilot $ Log.ProvingConditions Log.StepBisimulation
+     proveObls cruxOpts adapters clRefs Log.StepBisimulation simctx
+
+
+-- | Set up the "trigger override" functions.  These dummy functions
+--   take the place of the external functions called by the Copilot
+--   monitor when a guarded condition occurs.
+--
+--   Each trigger statement has a corresponding global variable that
+--   is used to record if the trigger function was called; initially
+--   the global is false, and is set to true when the trigger function
+--   is called.  At the end of verification, we check that the value
+--   of this global variable is true iff the corresponding trigger guard
+--   condition is true.
+--
+--   The other function of the trigger overrides is to check that, when called,
+--   the functions are given the expected argument values.
+--
+--   Otherwise, the override functions have no effects, which corresponds
+--   to the assumption that the external environment makes no changes to the
+--   program state that are observable to the Copilot monitor.
+triggerOverride :: forall sym t arch msgs.
+  IsSymInterface sym =>
+  Log.Logs msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+  (?intrinsicsOpts :: IntrinsicsOptions) =>
+  (1 <= ArchWidth arch) =>
+  HasPtrWidth (ArchWidth arch) =>
+  HasLLVMAnn sym =>
+
+  CopilotLogRefs sym ->
+  (Name, GlobalVar NatType, Pred sym) ->
+  (Name, BoolExpr t, [(Some Type, CW4.XExpr sym)]) ->
+  OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem
+triggerOverride clRefs (_,triggerGlobal,_) (nm, _guard, args) =
+   let args' = map toTypeRepr args in
+   case Ctx.fromList args' of
+     Some argCtx ->
+      basic_llvm_override $
+      LLVMOverride decl argCtx UnitRepr $
+        \memOps bak calledArgs ->
+          do let sym = backendGetSym bak
+             modifyGlobal triggerGlobal $ \count -> do
+               -- See Note [Global variables for trigger functions]
+               countPlusOne <- liftIO $ do
+                 one <- natLit sym 1
+                 natAdd sym count one
+               pure ((), countPlusOne)
+             mem <- readGlobal memOps
+             liftIO $ checkArgs bak mem (toListFC Some calledArgs) args
+             return ()
+
+ where
+  decl = L.Declare
+         { L.decLinkage = Nothing
+         , L.decVisibility = Nothing
+         , L.decRetType = L.PrimType L.Void
+         , L.decName = L.Symbol nm
+         , L.decArgs = map llvmArgTy args
+         , L.decVarArgs = False
+         , L.decAttrs = []
+         , L.decComdat = Nothing
+         }
+
+  -- Use the `-CompositePtr` functions here to ensure that arguments with array
+  -- or struct types are treated as pointers. See Note [Arrays and structs].
+  toTypeRepr (Some ctp, _) = llvmTypeAsRepr (copilotTypeToMemTypeCompositePtr (llvmDataLayout ?lc) ctp) Some
+  llvmArgTy (Some ctp, _) = copilotTypeToLLVMTypeCompositePtr ctp
+
+  checkArgs :: forall bak. IsSymBackend sym bak =>
+    bak -> MemImpl sym -> [Some (RegEntry sym)] -> [(Some Type, CW4.XExpr sym)] -> IO ()
+  checkArgs bak mem = loop (0::Integer)
+    where
+    loop i (x:xs) ((ctp,v):vs) = checkArg bak mem i x ctp v >> loop (i+1) xs vs
+    loop _ [] [] = return ()
+    loop _ _ _ = fail $ "Argument list mismatch in " ++ nm
+
+  checkArg :: forall bak. IsSymBackend sym bak =>
+    bak -> MemImpl sym -> Integer -> Some (RegEntry sym) -> Some Type -> CW4.XExpr sym -> IO ()
+  checkArg bak mem i (Some (RegEntry tp v)) (Some ctp) x =
+    do let sym = backendGetSym bak
+       eq <- computeEqualVals bak clRefs mem ctp x tp v
+       (ann, eq') <- annotateTerm sym eq
+       let shortmsg = "Trigger " ++ show nm ++ " argument " ++ show i
+       let longmsg  = show (printSymExpr eq')
+       let rsn      = AssertFailureSimError shortmsg longmsg
+       loc <- getCurrentProgramLoc sym
+       modifyIORef' (verifierAssertionMapRef clRefs)
+         $ Map.insert (BoolAnn ann)
+         $ Log.TriggerArgumentEqualityAssertion
+         $ Log.SomeSome
+         $ Log.TriggerArgumentEquality sym loc nm i ctp x tp v
+       addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))
+
+
+-- | Actually execute the Crucible simulator on the generated "step" function.
+--   This will record proof side-conditions into the symbolic backend, and
+--   return the memory state corresponding to the function post-state.
+--
+--   This function will record side-conditions that arise from the semantics
+--   of C itself (e.g., memory is accessed in bounds and signed arithmetic
+--   doesn't overflow) as well as the conditions related to trigger functions.
+executeStep :: forall sym arch msgs.
+  IsSymInterface sym =>
+  Log.Logs msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+  (?intrinsicsOpts :: IntrinsicsOptions) =>
+  (1 <= ArchWidth arch) =>
+  HasPtrWidth (ArchWidth arch) =>
+  HasLLVMAnn sym =>
+
+  VerifierOptions ->
+  CSettings ->
+  CopilotLogRefs sym ->
+  SimCtxt Crux sym LLVM ->
+  GlobalVar Mem ->
+  MemImpl sym ->
+  L.Module ->
+  ModuleTranslation arch ->
+  [(Name, GlobalVar NatType, Pred sym)] ->
+  [OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem] ->
+  [Pred sym] {- User-provided property assumptions -} ->
+  [Pred sym] {- Side conditions related to partial operations -} ->
+  IO (MemImpl sym)
+executeStep opts csettings clRefs simctx memVar mem llvmmod modTrans triggerGlobals triggerOverrides assums sideConds =
+  do globSt <- foldM setupTrigger (llvmGlobals memVar mem) triggerGlobals
+     let initSt = InitialState simctx globSt defaultAbortHandler memRepr $
+                    runOverrideSim memRepr runStep
+     res <- executeCrucible [] initSt
+     case res of
+       FinishedResult _ pr -> return (pr^.partialValue.gpValue.to regValue)
+       AbortedResult _ abortRes -> fail $ show $ ppAbortedResult abortRes
+       TimeoutResult{} -> fail "simulation timed out!"
+
+ where
+  -- See Note [Global variables for trigger functions]
+  setupTrigger gs (_,gv,_) = do
+    zero <- liftIO $ natLit sym 0
+    pure $ insertGlobal gv zero gs
+  llvm_ctx = modTrans ^. transContext
+  stepName = cSettingsStepFunctionName csettings
+  sym = simctx^.ctxSymInterface
+
+  -- TODO, would be lovely to be able to do better than dummy positions for all these things
+  -- so we can correspond assumptions and asserts back to the parts of the original spec that
+  -- gave rise to them.
+  dummyLoc = mkProgramLoc "<>" InternalPos
+
+  assumeProperty b =
+    withBackend simctx $ \bak ->
+      addAssumption bak (GenericAssumption dummyLoc "Property assumption" b)
+
+  assumeSideCond b =
+    withBackend simctx $ \bak ->
+      addAssumption bak (GenericAssumption dummyLoc "Side condition for partial operation" b)
+
+  ppAbortedResult :: AbortedResult sym ext -> PP.Doc ann
+  ppAbortedResult abortRes =
+    case gatherReasons abortRes of
+      reason :| [] -> reason
+      reasons      -> PP.vcat $ "Simulation aborted for multiple reasons."
+                              : NE.toList reasons
+
+  gatherReasons :: AbortedResult sym ext -> NonEmpty (PP.Doc ann)
+  gatherReasons (AbortedExec rsn _) =
+    PP.vcat ["Simulation aborted!", ppAbortExecReason rsn] :| []
+  gatherReasons (AbortedExit ec) =
+    PP.vcat ["Simulation called exit!", PP.viaShow ec] :| []
+  gatherReasons (AbortedBranch _ _ t f) =
+    gatherReasons t <> gatherReasons f
+
+  -- Simulator entry point
+  runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)
+  runStep =
+    do -- set up built-in functions and trigger overrides
+       register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx
+       -- set up functions defined in the module
+       registerLazyModule sayTranslationWarning modTrans
+
+       -- make any property assumptions
+       liftIO (mapM_ assumeProperty assums)
+
+       -- assume side conditions related to partial operations
+       when (assumePartialSideConds opts) $ liftIO $
+         mapM_ assumeSideCond sideConds
+
+       -- look up and call the step function
+       mbCfg <- liftIO $ getTranslatedCFG modTrans (L.Symbol stepName)
+       () <- case mbCfg of
+         Just (_, AnyCFG anyCfg, warns) -> do
+           liftIO $ mapM_ sayTranslationWarning warns
+           case (cfgArgTypes anyCfg, cfgReturnType anyCfg) of
+             (Empty, UnitRepr) -> regValue <$> callCFG anyCfg emptyRegMap
+             _ -> fail $ unwords [show stepName, "should take no arguments and return void"]
+         Nothing -> fail $ unwords ["Could not find step function named", show stepName]
+
+       -- Assert that the trigger functions were called exactly once iff the
+       -- associated guard condition was true.
+       -- See Note [Global variables for trigger functions].
+       forM_ triggerGlobals $ \(nm, gv, guard) ->
+         do expectedCount <- liftIO $ do
+              one  <- natLit sym 1
+              zero <- natLit sym 0
+              natIte sym guard one zero
+            actualCount <- readGlobal gv
+            eq <- liftIO $ natEq sym expectedCount actualCount
+            (ann, eq') <- liftIO $ annotateTerm sym eq
+            let shortmsg = "Trigger guard equality condition: " ++ show nm
+            let longmsg  = show (printSymExpr eq')
+            let rsn      = AssertFailureSimError shortmsg longmsg
+            liftIO
+              $ modifyIORef' (verifierAssertionMapRef clRefs)
+              $ Map.insert (BoolAnn ann)
+              $ Log.TriggersInvokedCorrespondinglyAssertion
+              $ Log.TriggersInvokedCorrespondingly dummyLoc nm expectedCount actualCount
+            withBackend simctx $ \bak ->
+              liftIO $ addDurableProofObligation bak (LabeledPred eq' (SimError dummyLoc rsn))
+
+       -- return the final state of the memory
+       readGlobal memVar
+
+-- | Given a bisimulation proof bundle and an empty initial state,
+--   populate the global ring-buffer variables with abstract state
+--   values, and write the abstract values of the external stream
+--   values into their proper locations.
+setupPrestate ::
+  IsSymBackend sym bak =>
+  HasPtrWidth wptr =>
+  HasLLVMAnn sym =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+
+  bak ->
+  MemImpl sym ->
+  CW4.BisimulationProofBundle sym ->
+  IO (MemImpl sym)
+setupPrestate bak mem0 prfbundle =
+  do mem' <- foldM setupStreamState mem0 (CW4.streamState (CW4.preStreamState prfbundle))
+     foldM setupExternalInput mem' (CW4.externalInputs prfbundle)
+
+ where
+   sym = backendGetSym bak
+
+   sizeTStorage :: StorageType
+   sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))
+
+   setupExternalInput mem (nm, Some ctp, v) =
+     do -- Compute LLVM/Crucible type information from the Copilot type
+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy
+        stType <- toStorableType memTy
+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)
+
+        -- resolve the global variable to a pointers
+        ptrVal <- doResolveGlobal bak mem (L.Symbol nm)
+
+        -- write the value into the global
+        regVal <- copilotExprToRegValue sym v typeRepr
+        doStore bak mem ptrVal typeRepr stType typeAlign regVal
+
+   setupStreamState mem (nm, Some ctp, vs) =
+     do -- TODO, should get these from somewhere inside copilot instead of building these names directly
+        let idxName = "s" ++ show nm ++ "_idx"
+        let bufName = "s" ++ show nm
+        let buflen  = genericLength vs :: Integer
+
+        -- Compute LLVM/Crucible type information from the Copilot type
+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
+        let typeLen    = memTypeSize (llvmDataLayout ?lc) memTy
+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy
+        stType <- toStorableType memTy
+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)
+
+        -- Resolve the global names into base pointers
+        idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)
+        bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)
+
+        -- Create a fresh index value in the proper range
+        idxVal <- freshBoundedBV sym (safeSymbol idxName) ?ptrWidth
+                     (Just 0) (Just (fromIntegral (buflen - 1)))
+        idxVal' <- llvmPointer_bv sym idxVal
+
+        -- store the index value in the correct location
+        let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))
+        mem' <- doStore bak mem idxPtr (LLVMPointerRepr ?ptrWidth) sizeTStorage sizeTAlign idxVal'
+
+        buflen'  <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)
+        typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))
+
+        -- Write each value of the stream ring buffer into its correct location
+        flip execStateT mem' $
+          forM_ (zip vs [0 ..]) $ \(v,i) ->
+            do ptrVal <- lift $
+                 do x1 <- bvAdd sym idxVal =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)
+                    x2 <- bvUrem sym x1 buflen'
+                    x3 <- bvMul sym x2 typeLen'
+                    ptrAdd sym ?ptrWidth bufPtr x3
+
+               regVal <- lift $ copilotExprToRegValue sym v typeRepr
+               StateT $ \m ->
+                 do m' <- doStore bak m ptrVal typeRepr stType typeAlign regVal
+                    return ((),m')
+
+-- | Given a memory image and a "proof state", assert that the global values
+--   for each stream ring buffer have values that correspond to the given
+--   stream state. This collection of assertions defines the bisimulation
+--   relation.
+assertStateRelation ::
+  IsSymBackend sym bak =>
+  Log.Logs msgs =>
+  HasPtrWidth wptr =>
+  HasLLVMAnn sym =>
+  (?memOpts :: MemOptions) =>
+  (?lc :: TypeContext) =>
+
+  bak ->
+  CopilotLogRefs sym ->
+  MemImpl sym ->
+  CW4.BisimulationProofState sym ->
+  IO ()
+assertStateRelation bak clRefs mem prfst =
+  -- For each stream in the proof state, assert that the
+  -- generated ring buffer global contains the corresponding
+  -- values.
+  forM_ (CW4.streamState prfst) assertStreamState
+
+ where
+   sym = backendGetSym bak
+
+   sizeTStorage :: StorageType
+   sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))
+
+   assertStreamState (nm, Some ctp, vs) =
+     do -- TODO, should get these from somewhere inside copilot instead of building these names directly
+        let idxName = "s" ++ show nm ++ "_idx"
+        let bufName = "s" ++ show nm
+        let buflen  = genericLength vs :: Integer
+
+        -- Compute LLVM/Crucible type information from the Copilot type
+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
+        let typeLen    = memTypeSize (llvmDataLayout ?lc) memTy
+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy
+        stType <- toStorableType memTy
+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)
+
+        -- Resolve the global names into base pointers
+        idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)
+        bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)
+
+        -- read the value of the ring buffer index
+        let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))
+        (bannIdxVal, pIdxVal, idxVal) <-
+          doLoadWithAnn bak mem idxPtr sizeTStorage (LLVMPointerRepr ?ptrWidth) sizeTAlign
+        idxVal' <- projectLLVM_bv bak idxVal
+        locIdxVal <- getCurrentProgramLoc sym
+        modifyIORef' (verifierAssertionMapRef clRefs)
+          $ Map.insert bannIdxVal
+          $ Log.RingBufferIndexLoadAssertion
+          $ Log.RingBufferIndexLoad sym locIdxVal (Text.pack idxName) pIdxVal
+
+        buflen'  <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)
+        typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))
+
+        -- For each value in the stream description, read a corresponding value from
+        -- memory and assert that they are equal.
+        forM_ (zip vs [0 ..]) $ \(v,i) ->
+          do ptrVal <-
+               do x1 <- bvAdd sym idxVal' =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)
+                  x2 <- bvUrem sym x1 buflen'
+                  x3 <- bvMul sym x2 typeLen'
+                  ptrAdd sym ?ptrWidth bufPtr x3
+
+             (bannv', pv', v') <- doLoadWithAnn bak mem ptrVal stType typeRepr typeAlign
+             locv' <- getCurrentProgramLoc sym
+             let bufNameT = Text.pack bufName
+             modifyIORef' (verifierAssertionMapRef clRefs)
+               $ Map.insert bannv'
+               $ Log.RingBufferLoadAssertion
+               $ Log.SomeSome
+               $ Log.RingBufferLoad sym locv' bufNameT i buflen ctp typeRepr pv'
+             eq <- computeEqualVals bak clRefs mem ctp v typeRepr v'
+             (ann, eq') <- annotateTerm sym eq
+             let shortmsg = "State equality condition: " ++ show nm ++ " index value " ++ show i
+             let longmsg  = show (printSymExpr eq')
+             let rsn      = AssertFailureSimError shortmsg longmsg
+             let loc      = mkProgramLoc "<>" InternalPos
+             modifyIORef' (verifierAssertionMapRef clRefs)
+               $ Map.insert (BoolAnn ann)
+               $ Log.StreamValueEqualityAssertion
+               $ Log.SomeSome
+               $ Log.StreamValueEquality sym loc bufNameT i buflen ctp v typeRepr v'
+             addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))
+
+        return ()
+
+-- | Translate the @XExpr@ values from the "Copilot.Theorem.What4" module into
+--   Crucible @RegValue@s suitable for injection into the Crucible simulator.
+copilotExprToRegValue :: forall sym tp.
+  IsSymInterface sym =>
+  sym ->
+  CW4.XExpr sym ->
+  TypeRepr tp ->
+  IO (RegValue sym tp)
+copilotExprToRegValue sym = loop
+  where
+    loop :: forall tp'. CW4.XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
+
+    loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @1) =
+      llvmPointer_bv sym =<< predToBV sym b knownRepr
+    loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
+      llvmPointer_bv sym =<< predToBV sym b knownRepr
+    loop (CW4.XInt8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
+      llvmPointer_bv sym x
+    loop (CW4.XInt16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =
+      llvmPointer_bv sym x
+    loop (CW4.XInt32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =
+      llvmPointer_bv sym x
+    loop (CW4.XInt64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =
+      llvmPointer_bv sym x
+    loop (CW4.XWord8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
+      llvmPointer_bv sym x
+    loop (CW4.XWord16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =
+      llvmPointer_bv sym x
+    loop (CW4.XWord32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =
+      llvmPointer_bv sym x
+    loop (CW4.XWord64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =
+      llvmPointer_bv sym x
+
+    loop (CW4.XFloat x)  (FloatRepr SingleFloatRepr) = return x
+    loop (CW4.XDouble x) (FloatRepr DoubleFloatRepr) = return x
+
+    loop CW4.XEmptyArray (VectorRepr _tpr) =
+      pure V.empty
+    loop (CW4.XArray xs) (VectorRepr tpr) =
+      V.generateM (PVec.lengthInt xs) (\i -> loop (PVec.elemAtUnsafe i xs) tpr)
+    loop (CW4.XStruct xs) (StructRepr ctx) =
+      Ctx.traverseWithIndex
+        (\i tpr -> RV <$> loop (xs !! Ctx.indexVal i) tpr)
+        ctx
+
+    loop x tpr =
+      fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show tpr]
+
+
+-- | Given an @XExpr@ from from the "Copilot.Theorem.What4" module, and
+--   a Crucible @RegValue@ which is expected to match, compute an equality
+--   predicate between the values.  The Crucible values may be pointers,
+--   requiring us to resolve the indirection through memory; this is necessary
+--   for array and struct values, but would also work for scalars.
+computeEqualVals :: forall sym bak tp a wptr.
+  IsSymBackend sym bak =>
+  HasPtrWidth wptr =>
+  HasLLVMAnn sym =>
+  (?lc :: TypeContext) =>
+  (?memOpts :: MemOptions) =>
+  bak ->
+  CopilotLogRefs sym ->
+  MemImpl sym ->
+  Type a ->
+  CW4.XExpr sym ->
+  TypeRepr tp ->
+  RegValue sym tp ->
+  IO (Pred sym)
+computeEqualVals bak clRefs mem = loop
+  where
+    sym = backendGetSym bak
+
+    loop :: forall tp' a'. Type a' -> CW4.XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
+    loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @1) =
+      isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v
+    loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
+      isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v
+    loop Int8 (CW4.XInt8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Int16 (CW4.XInt16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Int32 (CW4.XInt32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Int64 (CW4.XInt64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Word8 (CW4.XWord8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Word16 (CW4.XWord16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Word32 (CW4.XWord32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =
+      bvEq sym x =<< projectLLVM_bv bak v
+    loop Word64 (CW4.XWord64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =
+      bvEq sym x =<< projectLLVM_bv bak v
+
+    loop Float (CW4.XFloat x)  (FloatRepr SingleFloatRepr) v = iFloatEq @_ @SingleFloat sym x v
+    loop Double (CW4.XDouble x) (FloatRepr DoubleFloatRepr) v = iFloatEq @_ @DoubleFloat sym x v
+
+    loop (Array _ctp) CW4.XEmptyArray (VectorRepr _tpr) vs =
+      pure $ backendPred sym $ V.null vs
+    loop (Array ctp) (CW4.XArray xs) (VectorRepr tpr) vs
+      | PVec.lengthInt xs == V.length vs
+      = V.ifoldM (\pAcc i v -> andPred sym pAcc =<< loop ctp (PVec.elemAtUnsafe i xs) tpr v)
+                 (truePred sym) vs
+      | otherwise
+      = pure (falsePred sym)
+    loop (Struct struct) (CW4.XStruct xs) (StructRepr ctx) vs
+      | length copilotVals == Ctx.sizeInt (Ctx.size vs)
+      = ifoldlMFC (\i pAcc tpr ->
+                    case copilotVals !! Ctx.indexVal i of
+                      (Value ctp _, x) ->
+                        andPred sym pAcc =<< loop ctp x tpr (unRV (vs Ctx.! i)))
+                  (truePred sym) ctx
+      | otherwise
+      = pure (falsePred sym)
+      where
+        copilotVals :: [(Value a', CW4.XExpr sym)]
+        copilotVals = zip (toValues struct) xs
+
+    -- If we encounter a pointer, read the memory that it points to and recurse,
+    -- using the Copilot type as a guide for how much memory to read. This is
+    -- needed to make array- or struct-typed arguments work (see
+    -- Note [Arrays and structs]), although there is nothing about this code
+    -- that is array- or struct-specific. In fact, this code could also work
+    -- for pointer arguments of any other type.
+    loop ctp x PtrRepr v =
+      do let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
+             typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy
+         stp <- toStorableType memTy
+         llvmTypeAsRepr memTy $ \tpr ->
+           do loc <- getCurrentProgramLoc sym
+              (bann, p, regVal) <- doLoadWithAnn bak mem v stp tpr typeAlign
+              modifyIORef' (verifierAssertionMapRef clRefs)
+                $ Map.insert bann
+                $ Log.PointerArgumentLoadAssertion
+                $ Log.SomeSome
+                $ Log.PointerArgumentLoad sym loc ctp tpr p
+              loop ctp x tpr regVal
+
+    loop _ctp x tpr _v =
+      fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show tpr]
+
+-- | Convert a Copilot 'CT.Type' to a Crucible 'MemType'. 'CT.Bool's are
+-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.
+copilotTypeToMemType ::
+  DataLayout ->
+  CT.Type a ->
+  MemType
+copilotTypeToMemType dl = loop
+  where
+    loop :: forall t. CT.Type t -> MemType
+    loop CT.Bool   = i1
+    loop CT.Int8   = i8
+    loop CT.Int16  = i16
+    loop CT.Int32  = i32
+    loop CT.Int64  = i64
+    loop CT.Word8  = i8
+    loop CT.Word16 = i16
+    loop CT.Word32 = i32
+    loop CT.Word64 = i64
+    loop CT.Float  = FloatType
+    loop CT.Double = DoubleType
+    loop t0@(CT.Array tp) =
+      let len = fromIntegral (typeLength t0) in
+      ArrayType len (copilotTypeToMemTypeBool8 dl tp)
+    loop (CT.Struct v) =
+      StructType (mkStructInfo dl False (map val (CT.toValues v)))
+
+    val :: forall t. CT.Value t -> MemType
+    val (CT.Value tp _) = copilotTypeToMemTypeBool8 dl tp
+
+-- | Like 'copilotTypeToMemType', except that 'CT.Bool's are assumed to be
+-- eight bits, not one bit. See @Note [How LLVM represents bool]@.
+copilotTypeToMemTypeBool8 ::
+  DataLayout ->
+  CT.Type a ->
+  MemType
+copilotTypeToMemTypeBool8 _dl CT.Bool = i8
+copilotTypeToMemTypeBool8 dl tp = copilotTypeToMemType dl tp
+
+-- | Like 'copilotTypeToMemType', except that composite types (i.e.,
+-- 'CT.Array's and 'CT.Struct's) are converted to 'PtrType's instead of direct
+-- 'ArrayType's or 'StructType's. See @Note [Arrays and structs]@.
+copilotTypeToMemTypeCompositePtr ::
+  DataLayout ->
+  CT.Type a ->
+  MemType
+copilotTypeToMemTypeCompositePtr dl (CT.Array tp) =
+  PtrType (MemType (copilotTypeToMemTypeBool8 dl tp))
+copilotTypeToMemTypeCompositePtr _dl (CT.Struct struct) =
+  PtrType (Alias (copilotStructIdent struct))
+copilotTypeToMemTypeCompositePtr dl tp = copilotTypeToMemType dl tp
+
+-- | Convert a Copilot 'CT.Type' to an LLVM 'L.Type'. 'CT.Bool's are
+-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.
+copilotTypeToLLVMType ::
+  CT.Type a ->
+  L.Type
+copilotTypeToLLVMType = loop
+  where
+    loop :: forall t. CT.Type t -> L.Type
+    loop CT.Bool   = L.PrimType (L.Integer 1)
+    loop CT.Int8   = L.PrimType (L.Integer 8)
+    loop CT.Int16  = L.PrimType (L.Integer 16)
+    loop CT.Int32  = L.PrimType (L.Integer 32)
+    loop CT.Int64  = L.PrimType (L.Integer 64)
+    loop CT.Word8  = L.PrimType (L.Integer 8)
+    loop CT.Word16 = L.PrimType (L.Integer 16)
+    loop CT.Word32 = L.PrimType (L.Integer 32)
+    loop CT.Word64 = L.PrimType (L.Integer 64)
+    loop CT.Float  = L.PrimType (L.FloatType L.Float)
+    loop CT.Double = L.PrimType (L.FloatType L.Double)
+    loop t0@(CT.Array tp) =
+      let len = fromIntegral (typeLength t0) in
+      L.Array len (copilotTypeToLLVMTypeBool8 tp)
+    loop (CT.Struct v) =
+      -- NB: Don't use L.Struct here. That represents a literal, unnamed
+      -- struct, but all of the structs used in a copilot-c99 program are
+      -- named structs. As such, we must identify the struct by its alias.
+      L.Alias (copilotStructIdent v)
+
+-- | Like 'copilotTypeToLLVMType', except that 'CT.Bool's are assumed to be
+-- eight bits, not one bit. See @Note [How LLVM represents bool]@.
+copilotTypeToLLVMTypeBool8 ::
+  CT.Type a ->
+  L.Type
+copilotTypeToLLVMTypeBool8 CT.Bool = L.PrimType (L.Integer 8)
+copilotTypeToLLVMTypeBool8 tp = copilotTypeToLLVMType tp
+
+-- | Like 'copilotTypeToLLVMType', except that composite types (i.e.,
+-- 'CT.Array's and 'CT.Struct's) are given special treatment involving
+-- pointers. See @Note [Arrays and structs]@.
+copilotTypeToLLVMTypeCompositePtr ::
+  CT.Type a ->
+  L.Type
+copilotTypeToLLVMTypeCompositePtr (CT.Array tp) =
+  L.PtrTo (copilotTypeToLLVMTypeBool8 tp)
+copilotTypeToLLVMTypeCompositePtr (CT.Struct struct) =
+  L.PtrTo (L.Alias (copilotStructIdent struct))
+copilotTypeToLLVMTypeCompositePtr tp = copilotTypeToLLVMType tp
+
+-- | Given a struct @s@, construct the name @struct.s@ as an LLVM identifier.
+copilotStructIdent :: Struct a => a -> L.Ident
+copilotStructIdent struct = L.Ident $ "struct." ++ typeName struct
+
+{-
+Note [How LLVM represents bool]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+How are C values of type `bool` represented in LLVM? It depends. If it's being
+stored directly a `bool`, it's represented with `i1` (i.e., a single bit). If
+a `bool` is a member of some composite type, such as a pointer, array, or
+struct, however, it's representing with `i8` (i.e., eight bits). This means
+that we have to be careful when converting Bool-typed Copilot values, as they
+can become `i1` or `i8` depending on the context.
+
+copilot-verifier handles this by having both `copilotTypeToLLVMType` and
+`copilotTypeToLLVMTypeBool8` functions. The former function treats `bool`s as
+`i1`, whereas the latter treats `bool`s as `i8`. The former is used when
+converting "top-level" types (e.g., the argument types in a trigger override),
+whereas the latter is used when converting types that are part of a larger
+composite type (e.g., the element type in an array).
+
+The story for the `copilotTypeToMemType` and `copilotTypeToMemTypeBool8`
+functions is similar.
+
+Note [Arrays and structs]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When Clang compiles a function with an array argument, such as this trigger
+function:
+
+  void func(int32_t func_arg0[2]) { ... }
+
+It will produce the following LLVM code:
+
+  declare void @func(i32*) { ... }
+
+Note that the argument is an i32*, not a [2 x i32]. As a result, we can't
+translate Copilot array types directly to LLVM array types when they're used as
+arguments to a function. This impedance mismatch is handled in two places:
+
+1. The `copilotTypeToMemTypeCompositePtr`/`copilotTypeToLLVMTypeCompositePtr`
+   functions special-case Copilot arrays such that they are translated to
+   pointers. These functions are used when declaring the argument types of an
+   override for a trigger function (see `triggerOverride`).
+2. The `computeEqualVals` function has a special case for pointer
+   arguments—see the case that matches on `PtrRepr`. When a `PtrRepr` is
+   encountered, the underlying array values that it points to are read from
+   memory. Because `PtrRepr` doesn't record the type of the thing being pointed
+   to, `computeEqualVals` uses the corresponding Copilot type as a guide to
+   determine how much memory to read and at what type the memory should be
+   used. After this, `computeEqualVals` reads from the read array
+   element-by-element—see the `VectorRepr` cases.
+
+   Note that unlike `computeEqualVals`, `copilotExprToRegValue` does not need
+   a `PtrRepr` case. This is because `copilotExprToRegValue` is ultimately used
+   in service of calling writing elements of streams to memory, and streams do
+   not store pointer values (at least, not in today's Copilot).
+
+There is a very similar story for structs. Copilot passes structs by reference
+in trigger functions (e.g., `void trigger(struct s *ss)`), so we must also load
+from a `PtrRepr` in `computeEqualVals` to handle structs.
+
+See Note [Global variables for trigger functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As part of verifying that the behavior of a Copilot specification's trigger
+functions behave the same way as the trigger functions in the corresponding C
+program, we check that each trigger function in the C program is invoked the
+appropriate number of times. That is, if the guard condition for a trigger is
+true, the C trigger function should be invoked exactly once, and if the guard
+condition is false, then the trigger function should not be invoked at all.
+
+To check this, we create a Nat-valued global variable for each trigger function
+and initialize it to zero. Whenever we simulate a trigger function, we increment
+the value of the corresponding global variable. At the end of simulation, we
+check that the value in each global variable is equal to
+`if guard_cond then 1 else 0`.
+-}
+
+-- | Like @crucible-llvm@'s @doLoad@, but also returning the 'BoolAnn' and
+-- 'Pred' asserting the validity of the load.
+doLoadWithAnn ::
+  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
+  , ?memOpts :: MemOptions ) =>
+  bak ->
+  MemImpl sym ->
+  LLVMPtr sym wptr {- ^ pointer to load from      -} ->
+  StorageType      {- ^ type of value to load     -} ->
+  TypeRepr tp      {- ^ crucible type of the result -} ->
+  Alignment        {- ^ assumed pointer alignment -} ->
+  IO (BoolAnn sym, Pred sym, RegValue sym tp)
+doLoadWithAnn bak mem ptr valType tpr alignment = do
+    partLLVMVal <- loadRaw sym mem ptr valType alignment
+    (bann, p, llvmVal) <- assertSafeWithAnn bak partLLVMVal
+    regVal <- unpackMemValue sym tpr llvmVal
+    pure (bann, p, regVal)
+  where
+    sym = backendGetSym bak
+
+-- | Like @crucible-llvm@'s @assertSafe@, but also returning the 'BoolAnn' and
+-- 'Pred' corresponding the assertion.
+assertSafeWithAnn ::
+  IsSymBackend sym bak =>
+  bak ->
+  PartLLVMVal sym ->
+  IO (BoolAnn sym, Pred sym, LLVMVal sym)
+assertSafeWithAnn bak partVal =
+  case partVal of
+    NoErr p v -> do
+      (ann, p') <- annotateTerm sym p
+      assert bak p' rsn
+      return (BoolAnn ann, p', v)
+    Err p -> do
+      loc <- getCurrentProgramLoc sym
+      let err = SimError loc rsn
+      (_ann, p') <- annotateTerm sym p
+      addProofObligation bak (LabeledPred p' err)
+      abortExecBecause (AssertionFailure err)
+  where
+    rsn = AssertFailureSimError "Error during memory load" ""
+    sym = backendGetSym bak
+
+-- | Given a simulator state, extract any collected proof obligations,
+--   attempt to prove them, and present the results to the user.
+--
+--   Afterward, the simulator state will be cleared of any proof obligations,
+--   regardless of if they could all be proved.
+proveObls ::
+  IsSymInterface sym =>
+  sym ~ ExprBuilder t st fs =>
+  Log.Logs msgs =>
+  Log.SupportsCruxLogMessage msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  CruxOptions ->
+  [SolverAdapter st] ->
+  CopilotLogRefs sym ->
+  Log.VerificationStep ->
+  SimCtxt Crux sym LLVM ->
+  IO ()
+proveObls cruxOpts adapters clRefs step simctx =
+  withBackend simctx $ \bak ->
+  do let sym = backendGetSym bak
+     obls <- getProofObligations bak
+     clearProofObligations bak
+
+--     mapM_ (print . ppSimError) (summarizeObls sym obls)
+
+     vaMap <- readIORef $ verifierAssertionMapRef clRefs
+     let laMapRef = llvmAnnMapRef clRefs
+     laMap <- readIORef laMapRef
+     results <- proveGoalsOffline adapters cruxOpts simctx (explainFailure sym laMapRef) obls
+     presentResults sym vaMap laMap step results
+
+{-
+summarizeObls :: sym -> ProofObligations sym -> [SimError]
+summarizeObls _ Nothing = []
+summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList obls)
+-}
+
+presentResults ::
+  Log.Logs msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  IsSymInterface sym =>
+  sym ->
+  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->
+  LLVMAnnMap sym ->
+  Log.VerificationStep ->
+  (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) ->
+  IO ()
+presentResults sym vaMap laMap step (num, goals)
+  | numTotalGoals == 0
+  = Log.sayCopilot Log.AllGoalsProved
+
+    -- All goals were proven
+  | numProvedGoals == numTotalGoals
+  = do traverse_ (logVerifierAssertions sym vaMap laMap step num) goals
+       printGoals
+
+    -- There were some unproved goals, so fail with exit code 1
+  | otherwise
+  = do printGoals
+       exitFailure
+  where
+    numTotalGoals  = totalProcessedGoals num
+    numProvedGoals = provedGoals num
+
+    printGoals =
+      do Log.sayCopilot $ Log.OnlySomeGoalsProved numProvedGoals numTotalGoals
+         goals' <- provedGoalsTree sym goals
+         case goals' of
+           Just g -> Log.logGoal g
+           Nothing -> return ()
+
+-- | Upon a successful verification, log the various assertions that the
+-- verifier makes. These assertions will be visible in the output if the
+-- 'verbosity' is set to 'Noisy'.
+logVerifierAssertions ::
+  forall sym msgs.
+  IsSymInterface sym =>
+  Log.Logs msgs =>
+  Log.SupportsCopilotLogMessage msgs =>
+  sym ->
+  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->
+  LLVMAnnMap sym ->
+  Log.VerificationStep ->
+  ProcessedGoals ->
+  Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
+  IO ()
+logVerifierAssertions sym vaMap laMap step num goals = void $ go 0 goals
+  where
+    numTotalGoals = totalProcessedGoals num
+
+    go :: Integer ->
+          Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
+          IO Integer
+    go goalIdx gs =
+      case gs of
+        Assuming _ gs' ->
+          go goalIdx gs'
+
+        Prove (gl, locs, _) -> do
+          let p = gl^.labeledPred
+              nearestLoc = nearestProgramLoc locs
+
+          -- First, obtain the verifier assertion.
+          va <- case getAnnotation sym p of
+            -- If the assertion has a BoolAnn, look it up in the assertion maps
+            -- that we have accumulated during verification.
+            Just ann
+              |  Just va <- Map.lookup (BoolAnn ann) vaMap
+              -> pure va
+              |  Just (stk, bb) <- Map.lookup (BoolAnn ann) laMap
+              -> pure $ Log.LLVMBadBehaviorCheckAssertion
+                      $ Log.LLVMBadBehaviorCheck sym nearestLoc stk bb p
+              |  otherwise
+              -> fail $ unlines
+                   [ "Cannot find BoolAnn for assertion"
+                   , show $ gl^.labeledPredMsg
+                   , show $ printSymExpr p
+                   ]
+            -- If the assertion does not have a BoolAnn, fall back to using
+            -- heuristics to guess what kind of assertion it is.
+            Nothing -> pure $ verifierAssertionHeuristics sym nearestLoc p
+
+          -- Log the assertion.
+          case va of
+            Log.StreamValueEqualityAssertion (Log.SomeSome a) ->
+              Log.sayCopilot $
+              Log.StreamValueEqualityProofGoal step goalIdx numTotalGoals a
+            Log.TriggersInvokedCorrespondinglyAssertion a ->
+              Log.sayCopilot $
+              Log.TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals a
+            Log.TriggerArgumentEqualityAssertion (Log.SomeSome a) ->
+              Log.sayCopilot $
+              Log.TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals a
+            Log.RingBufferLoadAssertion (Log.SomeSome a) ->
+              Log.sayCopilot $
+              Log.RingBufferLoadProofGoal step goalIdx numTotalGoals a
+            Log.RingBufferIndexLoadAssertion a ->
+              Log.sayCopilot $
+              Log.RingBufferIndexLoadProofGoal step goalIdx numTotalGoals a
+            Log.PointerArgumentLoadAssertion (Log.SomeSome a) ->
+              Log.sayCopilot $
+              Log.PointerArgumentLoadProofGoal step goalIdx numTotalGoals a
+            Log.AccessorFunctionLoadAssertion a ->
+              Log.sayCopilot $
+              Log.AccessorFunctionLoadProofGoal step goalIdx numTotalGoals a
+            Log.GuardFunctionLoadAssertion a ->
+              Log.sayCopilot $
+              Log.GuardFunctionLoadProofGoal step goalIdx numTotalGoals a
+            Log.UnknownFunctionLoadAssertion a ->
+              Log.sayCopilot $
+              Log.UnknownFunctionLoadProofGoal step goalIdx numTotalGoals a
+            Log.LLVMBadBehaviorCheckAssertion a ->
+              Log.sayCopilot $
+              Log.LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals a
+
+          -- Finally, return the current goal index.
+          pure goalIdx
+
+        ProveConj gs1 gs2 -> do
+          goalIdx' <- go goalIdx gs1
+          go (goalIdx' + 1) gs2
+
+-- | If a verifier assertion does not have a corresponding 'BoolAnn', then we
+-- must use heuristics to guess what kind of assertion it is. These heuristics
+-- are not perfect, and we fall back to 'Log.UnknownFunctionLoad' in the event
+-- that we cannot figure out a more obvious cause for the assertion.
+verifierAssertionHeuristics ::
+  IsSymInterface sym =>
+  sym ->
+  ProgramLoc ->
+  Pred sym ->
+  Log.VerifierAssertion sym
+verifierAssertionHeuristics sym loc p
+  | "_get" `Text.isSuffixOf` functionName funName
+  = Log.AccessorFunctionLoadAssertion $
+    Log.AccessorFunctionLoad sym loc funName p
+
+  | "_guard" `Text.isSuffixOf` functionName funName
+  = Log.GuardFunctionLoadAssertion $
+    Log.GuardFunctionLoad sym loc funName p
+
+  | otherwise
+  = Log.UnknownFunctionLoadAssertion $
+    Log.UnknownFunctionLoad sym loc funName p
+  where
+    funName = plFunction loc
+
+-- | Pick the most recent 'ProgramLoc' in a trace of locations. If there are
+-- no locations available, return a dummy location.
+nearestProgramLoc :: [ProgramLoc] -> ProgramLoc
+nearestProgramLoc locs =
+  case locs of
+    loc:_ -> loc
+    _     -> mkProgramLoc "<>" InternalPos
+
+-- | A collection of 'IORef's used to accumulate log messages that the verifier
+-- may display at the end of verification.
+data CopilotLogRefs sym = CopilotLogRefs
+  { verifierAssertionMapRef :: !(IORef (Map.Map (BoolAnn sym) (Log.VerifierAssertion sym)))
+    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to 'Log.VerifierAssertions'.
+  , llvmAnnMapRef :: !(IORef (LLVMAnnMap sym))
+    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to assertions about checks
+    -- for bad behavior in LLVM.
+
+    -- This is kept in a separate 'IORef' for technical reasons, as
+    -- @crucible-llvm@'s 'explainFailure' function expects this 'IORef' as an
+    -- argument. We could put everything into 'verifierAssertionMapRef', but
+    -- that would require some tiresome 'IORef' massaging to make work.
+  }
+
+-- | Create a new 'CopilotLogRefs' value.
+newCopilotLogRefs :: IsSymInterface sym => IO (CopilotLogRefs sym)
+newCopilotLogRefs = do
+  vaMapRef <- newIORef mempty
+  laMapRef <- newIORef mempty
+  pure $ CopilotLogRefs
+    { verifierAssertionMapRef = vaMapRef
+    , llvmAnnMapRef = laMapRef
+    }
+
+data CopilotLogging
+  = LoggingCrux Log.CruxLogMessage
+  | LoggingCruxLLVM Log.CruxLLVMLogMessage
+  | LoggingCopilot Log.CopilotLogMessage
+  deriving stock Generic
+  deriving anyclass ToJSON
+
+copilotLoggingToSayWhat :: CopilotLogging -> Log.SayWhat
+copilotLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
+copilotLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
+copilotLoggingToSayWhat (LoggingCopilot msg) = Log.copilotLogMessageToSayWhat msg
+
+withCopilotLogging ::
+  ( ( Log.SupportsCruxLogMessage CopilotLogging
+    , Log.SupportsCruxLLVMLogMessage CopilotLogging
+    , Log.SupportsCopilotLogMessage CopilotLogging
+    ) => computation ) ->
+  computation
+withCopilotLogging computation = do
+  let ?injectCruxLogMessage = LoggingCrux
+      ?injectCruxLLVMLogMessage = LoggingCruxLLVM
+      ?injectCopilotLogMessage = LoggingCopilot
+    in computation
+
+sayTranslationWarning ::
+  Log.Logs msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  LLVMTranslationWarning -> IO ()
+sayTranslationWarning = Log.sayCruxLLVM . f
+  where
+    f (LLVMTranslationWarning s p msg) =
+        Log.TranslationWarning (Text.pack (show (ppSymbol s))) (Text.pack (show p)) msg
diff --git a/src/Copilot/Verifier/Log.hs b/src/Copilot/Verifier/Log.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Verifier/Log.hs
@@ -0,0 +1,729 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Copilot.Verifier.Log
+  ( SupportsCopilotLogMessage
+  , CopilotLogMessage(..)
+  , VerificationStep(..)
+  , VerifierAssertion(..)
+  , SomeSome(..)
+  , StreamValueEquality(..)
+  , TriggersInvokedCorrespondingly(..)
+  , TriggerArgumentEquality(..)
+  , RingBufferLoad(..)
+  , RingBufferIndexLoad(..)
+  , PointerArgumentLoad(..)
+  , AccessorFunctionLoad(..)
+  , GuardFunctionLoad(..)
+  , UnknownFunctionLoad(..)
+  , LLVMBadBehaviorCheck(..)
+  , sayCopilot
+  , copilotLogMessageToSayWhat
+  ) where
+
+import Crux (SayLevel (..), SayWhat (..))
+import qualified Crux.Log as Log
+import Data.Aeson (ToJSON (..), Value (..))
+import Data.Aeson.TH (defaultOptions, deriveToJSON)
+import Data.Kind (Type)
+import qualified Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.Vector as PV
+import qualified Data.Parameterized.TraversableFC.WithIndex as PWI
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Vector as V
+import GHC.Generics (Generic)
+import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.Text as PP
+
+import qualified Copilot.Core.Expr as CE
+import qualified Copilot.Core.Type as CT
+import qualified Copilot.Theorem.What4 as CW4
+
+import qualified Lang.Crucible.Simulator as LCS
+import qualified Lang.Crucible.Types as LCT
+import qualified Lang.Crucible.LLVM.Errors as LCLE
+import qualified Lang.Crucible.LLVM.Errors.MemoryError as LCLEME
+import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as LCLEUB
+import qualified Lang.Crucible.LLVM.MemModel as LCLM
+import qualified Lang.Crucible.LLVM.MemModel.CallStack as LCLMCS
+import qualified What4.FunctionName as WF
+import qualified What4.Interface as WI
+import qualified What4.ProgramLoc as WPL
+
+data CopilotLogMessage where
+  GeneratedCFile ::
+       FilePath
+       -- ^ The path of the generated C File
+    -> CopilotLogMessage
+  CompiledBitcodeFile ::
+       String
+       -- ^ The prefix to use in the compiled bitcode's directory
+    -> FilePath
+       -- ^ The name of the generated LLVM bitcode file
+    -> CopilotLogMessage
+  TranslatedToCrucible :: CopilotLogMessage
+  GeneratingProofState :: CopilotLogMessage
+  ComputingConditions :: VerificationStep -> CopilotLogMessage
+  ProvingConditions :: VerificationStep -> CopilotLogMessage
+  AllGoalsProved :: CopilotLogMessage
+  OnlySomeGoalsProved ::
+       Integer
+       -- ^ Number of goals proved
+    -> Integer
+       -- ^ Number of total goals
+    -> CopilotLogMessage
+
+  -----
+  -- Types of proof goals the verifier emits
+  --
+  -- The first three arguments to each constructor are:
+  --
+  -- * Which step of the verifier we are on
+  -- * The current goal number (zero-indexed)
+  -- * The total number of goals
+  -----
+
+  StreamValueEqualityProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> StreamValueEquality sym copilotType crucibleType
+    -> CopilotLogMessage
+
+  TriggersInvokedCorrespondinglyProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> TriggersInvokedCorrespondingly sym
+    -> CopilotLogMessage
+
+  TriggerArgumentEqualityProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> TriggerArgumentEquality sym copilotType crucibleType
+    -> CopilotLogMessage
+
+  RingBufferLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> RingBufferLoad sym copilotType crucibleType
+    -> CopilotLogMessage
+
+  RingBufferIndexLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> RingBufferIndexLoad sym
+    -> CopilotLogMessage
+
+  PointerArgumentLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> PointerArgumentLoad sym copilotType crucibleType
+    -> CopilotLogMessage
+
+  AccessorFunctionLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> AccessorFunctionLoad sym
+    -> CopilotLogMessage
+
+  GuardFunctionLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> GuardFunctionLoad sym
+    -> CopilotLogMessage
+
+  UnknownFunctionLoadProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> UnknownFunctionLoad sym
+    -> CopilotLogMessage
+
+  LLVMBadBehaviorCheckProofGoal ::
+       WI.IsSymExprBuilder sym
+    => VerificationStep
+    -> Integer
+    -> Integer
+    -> LLVMBadBehaviorCheck sym
+    -> CopilotLogMessage
+
+data VerificationStep
+  = InitialState
+  | StepBisimulation
+  deriving stock Generic
+  deriving anyclass ToJSON
+
+-- | Types of assertions that the verifier can make, which will count towards
+-- the total number of proof goals.
+data VerifierAssertion sym
+  = StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))
+  | TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)
+  | TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))
+  | RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))
+  | RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)
+  | PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))
+  | AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)
+  | GuardFunctionLoadAssertion (GuardFunctionLoad sym)
+  | UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)
+  | LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)
+
+-- | Like @Some@ in @parameterized-utils@, but existentially closing over two
+-- type parameters instead of just one.
+data SomeSome (f :: j -> k -> Type) where
+  SomeSome :: f x y -> SomeSome f
+
+-- | An assertion that an element in a Copilot stream is equal to the
+-- corresponding element in a C ring buffer.
+data StreamValueEquality sym copilotType crucibleType where
+  StreamValueEquality ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The locations of the values
+    -> Text
+       -- ^ The name of the buffer
+    -> Integer
+       -- ^ The offset from the buffer's index, which is used to compute the
+       -- element of the buffer to load
+    -> Integer
+       -- ^ The number of elements in the buffer
+    -> CT.Type copilotType
+       -- ^ The Copilot type
+    -> CW4.XExpr sym
+       -- ^ The Copilot value
+    -> LCT.TypeRepr crucibleType
+       -- ^ The Crucible type
+    -> LCS.RegValue sym crucibleType
+       -- ^ The Crucible value
+    -> StreamValueEquality sym copilotType crucibleType
+
+-- | An assertion that, given a Copilot trigger stream and its corresponding C
+-- trigger function on a particular time step, either both fired at the same
+-- time or both did not fire at all.
+data TriggersInvokedCorrespondingly sym where
+  TriggersInvokedCorrespondingly ::
+       WPL.ProgramLoc
+       -- ^ The location of the trigger
+    -> CE.Name
+       -- ^ The trigger name
+    -> WI.SymNat sym
+       -- ^ The expected number of times the trigger was fired this step
+       -- (should be either 1 or 0).
+    -> WI.SymNat sym
+       -- ^ The actual number of times the trigger was fired this step.
+    -> TriggersInvokedCorrespondingly sym
+
+-- | An assertion that an argument to a Copilot trigger is equal to the
+-- corresponding argument to a C trigger function.
+data TriggerArgumentEquality sym copilotType crucibleType where
+  TriggerArgumentEquality ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The locations of the arguments
+    -> CE.Name
+       -- ^ The trigger name
+    -> Integer
+       -- ^ The number of the argument (starting from 0)
+    -> CT.Type copilotType
+       -- ^ The Copilot type
+    -> CW4.XExpr sym
+       -- ^ The Copilot value
+    -> LCT.TypeRepr crucibleType
+       -- ^ The Crucible type
+    -> LCS.RegValue sym crucibleType
+       -- ^ The Crucible value
+    -> TriggerArgumentEquality sym copilotType crucibleType
+
+-- | An assertion that a load from a ring buffer in C is valid.
+data RingBufferLoad sym copilotType crucibleType where
+  RingBufferLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the trigger
+    -> Text
+       -- ^ The name of the buffer
+    -> Integer
+       -- ^ The offset from the buffer's index, which is used to compute the
+       -- element of the buffer to load
+    -> Integer
+       -- ^ The number of elements in the buffer
+    -> CT.Type copilotType
+       -- ^ The Copilot type of the elements of the array
+    -> LCT.TypeRepr crucibleType
+       -- ^ The Crucible type of the elements of the array
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> RingBufferLoad sym copilotType crucibleType
+
+-- | An assertion that a load from a global variable representing a ring
+-- buffer's index in C is valid.
+data RingBufferIndexLoad sym where
+  RingBufferIndexLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the trigger
+    -> Text
+       -- ^ The name of the global index
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> RingBufferIndexLoad sym
+
+-- | An assertion that a load from a pointer argument to a trigger function in C
+-- is valid.
+data PointerArgumentLoad sym copilotType crucibleType where
+  PointerArgumentLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the pointer
+    -> CT.Type copilotType
+       -- ^ The Copilot type of the underlying memory
+    -> LCT.TypeRepr crucibleType
+       -- ^ The Crucible type of the underlying memory
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> PointerArgumentLoad sym copilotType crucibleType
+
+-- | An assertion that a load occurring from somewhere in a stream accessor
+-- function in C (e.g., @s0_get@) is valid. This is a somewhat imprecise
+-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
+-- happens because of an array index.)
+data AccessorFunctionLoad sym where
+  AccessorFunctionLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the accessor function
+    -> WF.FunctionName
+       -- ^ The name of the accessor function
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> AccessorFunctionLoad sym
+
+-- | An assertion that a load occurring from somewhere in a trigger guard
+-- function in C (e.g., @even_guard@) is valid. This is a somewhat imprecise
+-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
+-- happens because of an array index.)
+data GuardFunctionLoad sym where
+  GuardFunctionLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the guard function
+    -> WF.FunctionName
+       -- ^ The name of the guard function
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> GuardFunctionLoad sym
+
+-- | An assertion that a load occurring in some function is valid. If you
+-- see this assertion, it is because the heuristics used to identify where
+-- load-related assertions come from could not identify a more precise cause
+-- for a load.
+data UnknownFunctionLoad sym where
+  UnknownFunctionLoad ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the function
+    -> WF.FunctionName
+       -- ^ The name of the function
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this load to be valid
+    -> UnknownFunctionLoad sym
+
+-- | An assertion that checks that some form of bad behavior in LLVM does not
+-- occur. Bad behavior includes both undefined behavior and memory unsafety.
+data LLVMBadBehaviorCheck sym where
+  LLVMBadBehaviorCheck ::
+       sym
+    -> WPL.ProgramLoc
+       -- ^ The location of the check
+    -> LCLMCS.CallStack
+       -- ^ A call stack for the check, if one exists
+    -> LCLE.BadBehavior sym
+       -- ^ What type of LLVM bad behavior is being checked for
+    -> WI.Pred sym
+       -- ^ The assertion that must hold in order for this check to succeed
+    -> LLVMBadBehaviorCheck sym
+
+-- Silly ToJSON instances. Crux is only requiring a ToJSON constraint for
+-- IDE-related functionality that we do not make use of, so the behavior of
+-- these instances aren't very important.
+
+instance ToJSON (StreamValueEquality sym copilotType crucibleType) where
+  toJSON _ = String "StreamValueEquality"
+
+instance ToJSON (TriggersInvokedCorrespondingly sym) where
+  toJSON _ = String "TriggersInvokedCorrespondingly"
+
+instance ToJSON (TriggerArgumentEquality sym copilotType crucibleType) where
+  toJSON _ = String "TriggerArgumentEquality"
+
+instance ToJSON (RingBufferLoad sym copilotType crucibleType) where
+  toJSON _ = String "RingBufferLoad"
+
+instance ToJSON (RingBufferIndexLoad sym) where
+  toJSON _ = String "RingBufferIndexLoad"
+
+instance ToJSON (PointerArgumentLoad sym copilotType crucibleType) where
+  toJSON _ = String "PointerArgumentLoad"
+
+instance ToJSON (AccessorFunctionLoad sym) where
+  toJSON _ = String "AccessorFunctionLoad"
+
+instance ToJSON (GuardFunctionLoad sym) where
+  toJSON _ = String "GuardFunctionLoad"
+
+instance ToJSON (UnknownFunctionLoad sym) where
+  toJSON _ = String "UnknownFunctionLoad"
+
+instance ToJSON (LLVMBadBehaviorCheck sym) where
+  toJSON _ = String "LLVMBadBehaviorCheck"
+
+type SupportsCopilotLogMessage msgs =
+  (?injectCopilotLogMessage :: CopilotLogMessage -> msgs)
+
+sayCopilot ::
+  Log.Logs msgs =>
+  SupportsCopilotLogMessage msgs =>
+  CopilotLogMessage ->
+  IO ()
+sayCopilot msg =
+  let ?injectMessage = ?injectCopilotLogMessage
+   in Log.say msg
+
+copilotTag :: Text
+copilotTag = "copilot-verifier"
+
+-- copilotFail :: Text -> SayWhat
+-- copilotFail = SayWhat Fail copilotTag
+
+copilotSimply :: Text -> SayWhat
+copilotSimply = SayWhat Simply copilotTag
+
+copilotNoisily :: Text -> SayWhat
+copilotNoisily = SayWhat Noisily copilotTag
+
+-- copilotWarn :: Text -> SayWhat
+-- copilotWarn = SayWhat Warn copilotTag
+
+copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat
+copilotLogMessageToSayWhat (GeneratedCFile csrc) =
+  copilotSimply $ "Generated " <> T.pack (show csrc)
+copilotLogMessageToSayWhat (CompiledBitcodeFile prefix bcFile) =
+  copilotSimply $ "Compiled " <> T.pack prefix <> " into " <> T.pack bcFile
+copilotLogMessageToSayWhat TranslatedToCrucible =
+  copilotSimply "Translated bitcode into Crucible"
+copilotLogMessageToSayWhat GeneratingProofState =
+  copilotSimply "Generating proof state data"
+copilotLogMessageToSayWhat (ComputingConditions step) =
+  copilotSimply $ "Computing " <> describeVerificationStep step <> " verification conditions"
+copilotLogMessageToSayWhat (ProvingConditions step) =
+  copilotSimply $ "Proving " <> describeVerificationStep step <> " verification conditions"
+copilotLogMessageToSayWhat AllGoalsProved =
+  copilotSimply "All obligations proved by concrete simplification"
+copilotLogMessageToSayWhat (OnlySomeGoalsProved numProvedGoals numTotalGoals) =
+  copilotSimply $ T.unwords
+    [ "Proved", T.pack (show numProvedGoals)
+    , "of"
+    , T.pack (show numTotalGoals), "total goals"
+    ]
+copilotLogMessageToSayWhat
+    (StreamValueEqualityProofGoal step goalIdx numTotalGoals
+      (StreamValueEquality
+        sym loc
+        bufName offset len
+        copilotTy copilotVal
+        crucibleTy crucibleVal)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the equality between two stream values"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Ring buffer name: " <> bufName
+    , "* Offset into buffer (from current index): " <> T.pack (show offset)
+    , "* Number of elements in buffer: " <> T.pack (show len)
+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")
+    , "* Copilot value:"
+    , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal
+    , "* Crucible value:"
+    , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal
+    ]
+copilotLogMessageToSayWhat
+    (TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals
+      (TriggersInvokedCorrespondingly loc name expected actual)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting triggers fired in corresponding ways"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Trigger name: " <> T.pack name
+    , "* Expected number of times trigger was fired:"
+    , renderStrict $ PP.indent 4 $ WI.printSymNat expected
+    , "* Actual number of times trigger was fired:"
+    , renderStrict $ PP.indent 4 $ WI.printSymNat actual
+    ]
+copilotLogMessageToSayWhat
+    (TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals
+      (TriggerArgumentEquality
+        sym loc
+        triggerName argNum
+        copilotTy copilotVal
+        crucibleTy crucibleVal)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the equality between two trigger arguments"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Trigger name: " <> T.pack triggerName
+    , "* Number of argument: " <> T.pack (show argNum)
+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")
+    , "* Copilot value:"
+    , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal
+    , "* Crucible value:"
+    , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal
+    ]
+copilotLogMessageToSayWhat
+    (RingBufferLoadProofGoal step goalIdx numTotalGoals
+      (RingBufferLoad
+        _sym loc bufName offset len copilotTy _crucibleTy p)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from a stream's ring buffer in C"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Ring buffer name: " <> bufName
+    , "* Offset into buffer (from current index): " <> T.pack (show offset)
+    , "* Number of elements in buffer: " <> T.pack (show len)
+    , "* Copilot type of buffer elements:" <> T.pack (showsCopilotType 0 copilotTy "")
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (RingBufferIndexLoadProofGoal step goalIdx numTotalGoals
+      (RingBufferIndexLoad _sym loc idxName p)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from the index to a stream's ring buffer in C"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Ring buffer index name: " <> idxName
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (PointerArgumentLoadProofGoal step goalIdx numTotalGoals
+      (PointerArgumentLoad
+        _sym loc copilotTy _crucibleTy p)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from a pointer argument to a trigger"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (AccessorFunctionLoadProofGoal step goalIdx numTotalGoals
+      (AccessorFunctionLoad _sym loc accessorName p)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from a stream accessor function"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Accessor function name: " <> WF.functionName accessorName
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (GuardFunctionLoadProofGoal step goalIdx numTotalGoals
+      (GuardFunctionLoad _sym loc accessorName p)) =
+  copilotNoisily $
+  displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from a trigger guard function"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Guard function name: " <> WF.functionName accessorName
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (UnknownFunctionLoadProofGoal step goalIdx numTotalGoals
+      (UnknownFunctionLoad _sym loc accessorName p)) =
+  copilotNoisily $
+    displayProofGoal
+    step goalIdx numTotalGoals
+    "asserting the validity of a memory load from an unknown function"
+    [ renderStrict $ ppProgramLoc loc
+    , "* Function name: " <> WF.functionName accessorName
+    , "* Validity predicate:"
+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+    ]
+copilotLogMessageToSayWhat
+    (LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals
+      (LLVMBadBehaviorCheck _sym loc stk bb p)) =
+  let ppLoc = renderStrict $ ppProgramLoc loc
+      ppCallStackLines =
+        [ "* Call stack:"
+        , "    " <> renderCallStack stk
+        ]
+      ppValidPredLines =
+        [ "* Validity predicate:"
+        , renderStrict $ PP.indent 4 $ WI.printSymExpr p
+        ] in
+  case bb of
+    LCLE.BBUndefinedBehavior ub ->
+      copilotNoisily $
+      displayProofGoal
+        step goalIdx numTotalGoals
+        "asserting that LLVM undefined behavior does not occur"
+        $ ppLoc : ppCallStackLines ++
+        [ "* Undefined behavior description:"
+        , renderStrict $ PP.indent 4 $ LCLEUB.ppDetails ub
+        ] ++ ppValidPredLines
+    LCLE.BBMemoryError me ->
+      copilotNoisily $
+      displayProofGoal
+        step goalIdx numTotalGoals
+        "asserting that LLVM memory unsafety does not occur"
+        $ ppLoc : ppCallStackLines ++
+        [ "* Memory unsafety description:"
+        , renderStrict $ PP.indent 4 $ LCLEME.explain me
+        ] ++ ppValidPredLines
+
+describeVerificationStep :: VerificationStep -> Text
+describeVerificationStep InitialState     = "initial state"
+describeVerificationStep StepBisimulation = "step bisimulation"
+
+-- | Display information about an emitted proof goal.
+displayProofGoal ::
+     VerificationStep
+  -> Integer
+  -> Integer
+  -> Text
+  -> [Text]
+  -> Text
+displayProofGoal step goalIdx numTotalGoals why ls = T.unlines $
+  [ banner
+  , "Emitted a proof goal (" <> why <> ")"
+  , "  During the " <> displayStep
+  , "  Proof goal " <> T.pack (show goalIdx)
+                    <> " ("
+                    <> T.pack (show numTotalGoals)
+                    <> " total)"
+  , ""
+  ]
+  ++ ls ++ [banner]
+  where
+    banner = "====="
+    displayStep =
+      case step of
+        InitialState ->
+          "initial bisimulation state step"
+        StepBisimulation ->
+          "transition step of bisimulation"
+
+ppProgramLoc :: WPL.ProgramLoc -> PP.Doc a
+ppProgramLoc pl = PP.vcat
+  [ "* Function:" PP.<+> PP.pretty (WPL.plFunction pl)
+  , "  Position:" PP.<+> PP.pretty (WPL.plSourceLoc pl)
+  ]
+
+renderCallStack :: LCLMCS.CallStack -> Text
+renderCallStack cs
+  | T.null ppText
+  = "<no call stack available>"
+  | otherwise
+  = ppText
+  where
+    ppText = renderStrict $ LCLMCS.ppCallStack cs
+
+showsCopilotType :: Int -> CT.Type tp -> ShowS
+showsCopilotType prec tp =
+  case tp of
+    CT.Bool     -> showString "Bool"
+    CT.Int8     -> showString "Int8"
+    CT.Int16    -> showString "Int16"
+    CT.Int32    -> showString "Int32"
+    CT.Int64    -> showString "Int64"
+    CT.Word8    -> showString "Word8"
+    CT.Word16   -> showString "Word16"
+    CT.Word32   -> showString "Word32"
+    CT.Word64   -> showString "Word64"
+    CT.Float    -> showString "Float"
+    CT.Double   -> showString "Double"
+    CT.Array t  -> showParen (prec >= 11) $
+                     showString "Array" .
+                     showsPrec 11 (CT.typeSize tp) .
+                     showsCopilotType 11 t
+    CT.Struct x -> showString $ CT.typeName x
+
+ppCopilotValue :: WI.IsSymExprBuilder sym => CW4.XExpr sym -> PP.Doc a
+ppCopilotValue val =
+  case val of
+    CW4.XBool   b -> WI.printSymExpr b
+    CW4.XInt8   i -> WI.printSymExpr i
+    CW4.XInt16  i -> WI.printSymExpr i
+    CW4.XInt32  i -> WI.printSymExpr i
+    CW4.XInt64  i -> WI.printSymExpr i
+    CW4.XWord8  w -> WI.printSymExpr w
+    CW4.XWord16 w -> WI.printSymExpr w
+    CW4.XWord32 w -> WI.printSymExpr w
+    CW4.XWord64 w -> WI.printSymExpr w
+    CW4.XFloat  f -> WI.printSymExpr f
+    CW4.XDouble d -> WI.printSymExpr d
+    CW4.XEmptyArray -> "[]"
+    CW4.XArray  a   -> ppBracesWith ppCopilotValue (PV.toList a)
+    CW4.XStruct s   -> ppBracketsWith ppCopilotValue s
+
+ppCrucibleValue :: WI.IsSymExprBuilder sym
+                => sym
+                -> LCT.TypeRepr tp
+                -> LCS.RegValue sym tp
+                -> PP.Doc a
+ppCrucibleValue sym tp val =
+  case tp of
+    LCLM.LLVMPointerRepr _ -> LCLM.ppPtr val
+    LCT.FloatRepr _        -> WI.printSymExpr val
+    LCT.VectorRepr tpr     -> ppBracketsWith (ppCrucibleValue sym tpr) (V.toList val)
+    LCT.StructRepr ctx     -> withBraces $
+                              PWI.itoListFC (\i (LCS.RV v) -> ppCrucibleValue sym (ctx Ctx.! i) v) val
+    _ -> error $ "ppCrucibleValue: Unsupported type: " ++ show tp
+
+renderStrict :: PP.Doc a ->  Text
+renderStrict = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions
+
+ppBracketsWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
+ppBracketsWith f = PP.align . PP.list . map f
+
+ppBracesWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
+ppBracesWith f = withBraces . map f
+
+withBraces :: [PP.Doc a] -> PP.Doc a
+withBraces =
+    PP.align
+  . PP.encloseSep (PP.flatAlt "{ " "{") (PP.flatAlt " }" "}") ", "
+
+$(deriveToJSON defaultOptions ''CopilotLogMessage)
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,32 @@
+module Main (main) where
+
+import qualified Data.CaseInsensitive as CI
+import qualified Data.Map as Map
+import qualified Data.Text as Text
+import System.IO (stderr, stdout)
+import System.IO.Silently (hSilence)
+import Test.Tasty
+import Test.Tasty.ExpectedFailure
+import Test.Tasty.HUnit
+
+import Copilot.Verifier (Verbosity(..))
+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)
+
+main :: IO ()
+main = defaultMain $
+  testGroup "copilot-verifier-examples tests"
+    [ testGroup "should-fail tests" $
+        -- Why use hSilence for the should-fail tests when we are passing
+        -- Quiet? It's because crux-llvm errors are logged at the highest
+        -- severity possible, and even Crux's quietMode isn't enough to
+        -- suppress those messages. We could try messing with things on the
+        -- Crux side to avoid this, but it's simpler just to use hSilence here.
+        -- After all, we don't really care about the output of failing tests
+        -- anyway, just their exit codes.
+        map (\(name, action) -> expectFail (testCase (Text.unpack (CI.original name))
+                                                     (hSilence [stderr, stdout] action)))
+            (Map.toAscList (shouldFailExamples Quiet))
+    , testGroup "should-pass tests" $
+        map (\(name, action) -> testCase (Text.unpack (CI.original name)) action)
+            (Map.toAscList (shouldPassExamples Quiet))
+    ]