From f53de1e903e7cbadfd7de076ed7ed27508f1c822 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:16:22 -0500
Subject: [PATCH 01/32] Fill in 0.1 CHANGELOG entry for crucible-mir

This is copy-pasted from the `crux-mir` CHANGELOG, as both libraries were
involved in coordinated changes.

(cherry picked from commit 668b81f3b23f60c0137ec867de701b86f862cec7)
---
 crucible-mir/CHANGELOG.md | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 59762abdc..64ce88063 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,3 +1,15 @@
 # 0.1
 
-* TODO: Describe API changes here
+* Much of the `crux-mir` library has been split off into a `crucible-mir`
+  library, which removes all of the `crux`-specific code. The following modules
+  were _not_ migrated to `crucible-mir`:
+
+  * `Mir.Generate`
+  * `Mir.Language`
+  * `Mir.Log`
+  * `Mir.Concurrency`
+  * `Mir.Overrides`
+
+  Note that `Mir.Generate` now only exports the `generateMIR` function. The
+  `parseMIR` and `translateMIR` functions have been moved to a new
+  `Mir.ParseTranslate` module in `crucible-mir`.

From 0f275cd9eb1b5e8447165350da7150358c8d3f59 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:21:31 -0500
Subject: [PATCH 02/32] Mention #1096 in the {crucible,crux}-mir CHANGELOGs

(cherry picked from commit cd845993e5b9f5403fe595c1231450d86a707fa5)
---
 crucible-mir/CHANGELOG.md | 13 +++++++++++++
 crux-mir/CHANGELOG.md     | 13 +++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 64ce88063..7d54558c2 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,3 +1,16 @@
+# next
+
+* `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of
+  the highlights of this include:
+
+  * Properly support for Rust's new constant forms
+  * Better support for zero-sized constants
+  * Encoding enum discriminant types so that `crucible-mir` can know about
+    non-`isize` discriminant types (e.g., `Ordering`, which uses an `i8`
+    discriminant)
+  * A more intelligent way of computing crate disambiguators for looking up
+    known types such as `MaybeUninit` and `Option`
+
 # 0.1
 
 * Much of the `crux-mir` library has been split off into a `crucible-mir`
diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index 67282381f..16d72b97f 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -1,3 +1,16 @@
+# next
+
+* `crux-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of the
+   highlights of this include:
+
+  * Properly support for Rust's new constant forms
+  * Better support for zero-sized constants
+  * Encoding enum discriminant types so that `crux-mir` can know about
+    non-`isize` discriminant types (e.g., `Ordering`, which uses an `i8`
+    discriminant)
+  * A more intelligent way of computing crate disambiguators for looking up
+    known types such as `MaybeUninit` and `Option`
+
 # 0.7 -- 2023-06-26
 
 ## API changes

From 89ca671532ae27635b64aa192b7ada3014ef5669 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:25:26 -0500
Subject: [PATCH 03/32] Mention #1106 in the crucible-mir CHANGELOG

(cherry picked from commit e1dec5c3f76a0af7a4954cb454af28ef721feaa7)
---
 crucible-mir/CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 7d54558c2..8575fa1ae 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -10,6 +10,11 @@
     discriminant)
   * A more intelligent way of computing crate disambiguators for looking up
     known types such as `MaybeUninit` and `Option`
+* Functions in `Mir.Intrinsics` now avoid taking or returning `SimState` values
+  as arguments, instead preferring `SymGlobalState` and `IntrinsicTypes`. This
+  makes it possible to call into the `crucible-mir` memory model from SAW
+  without needing a full-blown `SimState`, which isn't readily at hand in the
+  parts of SAW that need the memory model.
 
 # 0.1
 

From 381cc6bc894f9e6279d7fdb849787ec153fe6bd4 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:28:39 -0500
Subject: [PATCH 04/32] Mention #1107 in the crucible-mir CHANGELOG

(cherry picked from commit b9ff7231990c57ca0e384cba5e9e55a9a63717a1)
---
 crucible-mir/CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 8575fa1ae..4ca879124 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -15,6 +15,10 @@
   makes it possible to call into the `crucible-mir` memory model from SAW
   without needing a full-blown `SimState`, which isn't readily at hand in the
   parts of SAW that need the memory model.
+* There are now variants of the memory model–related functions in
+  `Mir.Intrinsics` whose names are suffixed with `*IO`. These functions live in
+  `IO` instead of `MuxLeafT sym IO`, which make them easier to call from `IO`
+  contexts.
 
 # 0.1
 

From 58395e8537bbdd13f5e237b71a5886413f2e6143 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:31:35 -0500
Subject: [PATCH 05/32] Mention #1110 in the crucible-llvm CHANGELOG

(cherry picked from commit dfe84faa56b25c3383cd07271891f59ff41253c1)
---
 crucible-llvm/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index 811beceb3..e99e12bf6 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -2,6 +2,8 @@
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.
   Use `decName` to get a `Symbol` from a `Declare`.
+* Implement overrides for the LLVM `llvm.is.fpclass.f*` intrinsics.
+* Implement overrides for the `isinf`, `__isinf`, and `__isinff` C functions.
 
 # 0.5
 * Add `?memOpts :: MemOptions` constraints to the following functions:

From 1746bb391e625d0b40ede70011065adc7d32811e Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:36:15 -0500
Subject: [PATCH 06/32] Add CHANGELOGs for crucible-cli, crucible-llvm-cli,
 crucible-llvm-syntax

(cherry picked from commit 3b3b5a5fac6453797d1f0d1a96483ee6e0e26977)
---
 crucible-cli/CHANGELOG.md                       | 3 +++
 crucible-cli/crucible-cli.cabal                 | 2 +-
 crucible-llvm-cli/CHANGELOG.md                  | 3 +++
 crucible-llvm-cli/crucible-llvm-cli.cabal       | 2 +-
 crucible-llvm-syntax/CHANGELOG.md               | 3 +++
 crucible-llvm-syntax/crucible-llvm-syntax.cabal | 2 +-
 6 files changed, 12 insertions(+), 3 deletions(-)
 create mode 100644 crucible-cli/CHANGELOG.md
 create mode 100644 crucible-llvm-cli/CHANGELOG.md
 create mode 100644 crucible-llvm-syntax/CHANGELOG.md

diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md
new file mode 100644
index 000000000..956a58949
--- /dev/null
+++ b/crucible-cli/CHANGELOG.md
@@ -0,0 +1,3 @@
+# next
+
+* TODO: Describe API changes here
diff --git a/crucible-cli/crucible-cli.cabal b/crucible-cli/crucible-cli.cabal
index 3ed59bd14..ec925bb05 100644
--- a/crucible-cli/crucible-cli.cabal
+++ b/crucible-cli/crucible-cli.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A library for sharing code between Crucible CLI frontends
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/**/*.cbl
   test-data/**/*.out.good
diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md
new file mode 100644
index 000000000..956a58949
--- /dev/null
+++ b/crucible-llvm-cli/CHANGELOG.md
@@ -0,0 +1,3 @@
+# next
+
+* TODO: Describe API changes here
diff --git a/crucible-llvm-cli/crucible-llvm-cli.cabal b/crucible-llvm-cli/crucible-llvm-cli.cabal
index 53c282bab..c10704349 100644
--- a/crucible-llvm-cli/crucible-llvm-cli.cabal
+++ b/crucible-llvm-cli/crucible-llvm-cli.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A Crucible CLI frontend for the LLVM language extension
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/*.cbl
   test-data/*.out.good
diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md
new file mode 100644
index 000000000..956a58949
--- /dev/null
+++ b/crucible-llvm-syntax/CHANGELOG.md
@@ -0,0 +1,3 @@
+# next
+
+* TODO: Describe API changes here
diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index 94283e72a..04d436f0a 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A syntax for reading and writing Crucible-LLVM control-flow graphs
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/*.cbl
   test-data/*.out.good

From 3a191e58026f4dabdf65a15177243ceb0fc19088 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:38:42 -0500
Subject: [PATCH 07/32] Mention #1123 in the crucible-syntax CHANGELOG

(cherry picked from commit 3bb0064c443e54298882b653f7860b023aa3c171)
---
 crucible-syntax/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md
index 0c4925904..3b76ffbcb 100644
--- a/crucible-syntax/CHANGELOG.md
+++ b/crucible-syntax/CHANGELOG.md
@@ -4,6 +4,8 @@
   which serves a similar purpose (hiding the argument and return types). The
   CFG argument and return types can be recovered via
   `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`.
+* `execCommand` and related data types in `Lang.Crucible.Syntax.Prog` have been
+  split off into a separate `crucible-cli` library.
 
 # 0.3
 

From da57d3fff352d933242cd394549a60e7b5fbe2bf Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:42:41 -0500
Subject: [PATCH 08/32] Mention #1121 in the crucible-syntax CHANGELOG

(cherry picked from commit 8c302b7ba8e02cf4370875758e10c8ac39a63314)
---
 crucible-syntax/CHANGELOG.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md
index 3b76ffbcb..4bb8af8ce 100644
--- a/crucible-syntax/CHANGELOG.md
+++ b/crucible-syntax/CHANGELOG.md
@@ -4,6 +4,14 @@
   which serves a similar purpose (hiding the argument and return types). The
   CFG argument and return types can be recovered via
   `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`.
+* `crucible-syntax` now supports simulating CFGs with language-specific syntax
+  extensions:
+
+  * `SimulateProgramHooks` now has a `setupHook` field that can run an arbitrary
+    override action before simulation. (For example, this is used in
+    `crucible-llvm-syntax` to initialize the LLVM memory global variable.)
+  * `SimulateProgramHooks` now has an extra `ext` type variable so that hooks
+    can be extension-specific.
 * `execCommand` and related data types in `Lang.Crucible.Syntax.Prog` have been
   split off into a separate `crucible-cli` library.
 

From 43d1fa40ddee021b3e940be8e75baba4a7e1156d Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:49:15 -0500
Subject: [PATCH 09/32] Mention #1136 in the relevant CHANGELOGs

(cherry picked from commit 6d85c60237158e9d9137e99cf33a7e5bdc792e74)
---
 crucible-go/CHANGELOG.md  | 3 ++-
 crucible-jvm/CHANGELOG.md | 3 ++-
 crucible/CHANGELOG.md     | 4 ++++
 crux/CHANGELOG.md         | 5 +++++
 4 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md
index 956a58949..512f2eb05 100644
--- a/crucible-go/CHANGELOG.md
+++ b/crucible-go/CHANGELOG.md
@@ -1,3 +1,4 @@
 # next
 
-* TODO: Describe API changes here
+* Change `SomeOverride`, as well as related functions in
+  `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`.
diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md
index 956a58949..36dc6c410 100644
--- a/crucible-jvm/CHANGELOG.md
+++ b/crucible-jvm/CHANGELOG.md
@@ -1,3 +1,4 @@
 # next
 
-* TODO: Describe API changes here
+* Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a
+  `TypedOverride`.
diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
index f6ebac5bf..c24037b8d 100644
--- a/crucible/CHANGELOG.md
+++ b/crucible/CHANGELOG.md
@@ -2,6 +2,10 @@
 
 * Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`,
   provide helpers such as `popFrame` to manage assumptions without `panic`ing.
+* Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to
+  `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an
+  `OverrideSim` action and bundle `TypeRepr`s for its argument and result
+  types, which is a common pattern in several Crucible backends.
 
 # 0.6
 
diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
index 875f684b1..dcf53179b 100644
--- a/crux/CHANGELOG.md
+++ b/crux/CHANGELOG.md
@@ -1,3 +1,8 @@
+# next
+
+* Add a `Crux.Overrides` module, which defines common functionality for defining
+  overrides, which are shared among several Crux backends.
+
 # 0.6
 
 * Corresponds to the 0.6 release of `crux-llvm` and `crux-mir`.

From de731ba1d415d354060f13544c70848108864bb2 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:50:16 -0500
Subject: [PATCH 10/32] Mention #1151 in the crucible CHANGELOG

(cherry picked from commit 40d96fe0c90189ce915561b30f10b68e19c200b7)
---
 crucible/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
index c24037b8d..947281966 100644
--- a/crucible/CHANGELOG.md
+++ b/crucible/CHANGELOG.md
@@ -6,6 +6,8 @@
   `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an
   `OverrideSim` action and bundle `TypeRepr`s for its argument and result
   types, which is a common pattern in several Crucible backends.
+* Add `Lang.Crucible.Simulator.OverrideSim.bindCFG`, a utility function for
+  binding a CFG to its handle in an `OverrideSim`.
 
 # 0.6
 

From fd2351d34a787e872d7ee566ff32080d9de1c3ca Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:53:01 -0500
Subject: [PATCH 11/32] Mention #1155 in the crucible-llvm CHANGELOG

(cherry picked from commit e6559dbbb91c1729c0b518019c4d1d26207e0dd1)
---
 crucible-llvm/CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index e99e12bf6..31dc8654a 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -4,6 +4,9 @@
   Use `decName` to get a `Symbol` from a `Declare`.
 * Implement overrides for the LLVM `llvm.is.fpclass.f*` intrinsics.
 * Implement overrides for the `isinf`, `__isinf`, and `__isinff` C functions.
+* Implement overrides for the LLVM `llvm.fma.f*` and `llvm.fmuladd.f*`
+  intrinsics.
+* Implement overrides for the `fma` and `fmaf` C functions.
 
 # 0.5
 * Add `?memOpts :: MemOptions` constraints to the following functions:

From ccc70542c5ee7b14d23ec7c02df6a67e92fd3cfc Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:53:41 -0500
Subject: [PATCH 12/32] Mention #1141 in the CHANGELOG

(cherry picked from commit 5fb4da5a1d7e170182f2c619f1a763b1a3a01d3b)
---
 crucible-mir/CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 4ca879124..3714f7f89 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -19,6 +19,7 @@
   `Mir.Intrinsics` whose names are suffixed with `*IO`. These functions live in
   `IO` instead of `MuxLeafT sym IO`, which make them easier to call from `IO`
   contexts.
+* Support enums marked with `repr(transparent)`.
 
 # 0.1
 

From cc810f430f6bffb023b89f9fb3be86869186a05e Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:54:55 -0500
Subject: [PATCH 13/32] Mention #1158 in the CHANGELOG

(cherry picked from commit bc05b99e38f13e0f98f670eed3ac60bf06945674)
---
 crucible-mir/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 3714f7f89..933a08925 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -20,6 +20,8 @@
   `IO` instead of `MuxLeafT sym IO`, which make them easier to call from `IO`
   contexts.
 * Support enums marked with `repr(transparent)`.
+* Fix a bug in which the custom overrides for `rotate_left` and related
+  intrinsics were not applied.
 
 # 0.1
 

From c36a69d197b7ac0dcd4ce23385e6f04697d859e6 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:56:01 -0500
Subject: [PATCH 14/32] Mention #1157 in the crux-mir CHANGELOG

(cherry picked from commit e1fc9f8169889fa98b5cb32d5a927a1790c0399b)
---
 crux-mir/CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index 16d72b97f..3d68c9b91 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -10,6 +10,7 @@
     discriminant)
   * A more intelligent way of computing crate disambiguators for looking up
     known types such as `MaybeUninit` and `Option`
+* Support code that uses `vec::IntoIter` on length-0 `Vec` values.
 
 # 0.7 -- 2023-06-26
 

From c33bed5d569016eb7e24dbfc49363e5b70e8e755 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:56:38 -0500
Subject: [PATCH 15/32] Mention #1163 in the crucible-llvm CHANGELOG

(cherry picked from commit 86ae4d78017750371bd051076e05370f481bb5ef)
---
 crucible-llvm/CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index 31dc8654a..c453214b2 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -7,6 +7,7 @@
 * Implement overrides for the LLVM `llvm.fma.f*` and `llvm.fmuladd.f*`
   intrinsics.
 * Implement overrides for the `fma` and `fmaf` C functions.
+* Add a `Lang.Crucible.LLVM.MemModel.CallStack.null` function.
 
 # 0.5
 * Add `?memOpts :: MemOptions` constraints to the following functions:

From 615a3dcf3fdcfc9bcc3d09a3551e4f5cbef623f1 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 15:58:37 -0500
Subject: [PATCH 16/32] Mention #1162 in the crucible-llvm CHANGELOG

(cherry picked from commit 6f940c10ab79e0a8e963f4be6ee214179a5d395c)
---
 crucible-llvm/CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index c453214b2..9129b111f 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -8,6 +8,11 @@
   intrinsics.
 * Implement overrides for the `fma` and `fmaf` C functions.
 * Add a `Lang.Crucible.LLVM.MemModel.CallStack.null` function.
+* Add a `ppLLVMLatest` function to `Lang.Crucible.LLVM.PrettyPrint`, which
+  pretty-prints an LLVM AST using the latest LLVM version that `llvm-pretty`
+  currently supports. Also add derived combinators (`ppDeclare`, `ppIdent`,
+  etc.) for calling the `llvm-pretty` functions of the same names in tandem
+  with `ppLLVMLatest`.
 
 # 0.5
 * Add `?memOpts :: MemOptions` constraints to the following functions:

From d2cad43738769c18f4a40dad73c1fbc38d7aaf76 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:04:46 -0500
Subject: [PATCH 17/32] Add source-repository stanzas

(cherry picked from commit 111c6a42ff030db7590725ec9a0608b59f0367ad)
---
 crucible-llvm/crucible-llvm.cabal   | 5 +++++
 crucible-symio/crucible-symio.cabal | 5 +++++
 crucible/crucible.cabal             | 5 +++++
 crux-llvm/crux-llvm.cabal           | 5 +++++
 crux/crux.cabal                     | 5 +++++
 5 files changed, 25 insertions(+)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index 603d1325a..1913ba973 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -14,6 +14,11 @@ Description:
    for Crucible-based simulation and verification of LLVM-compiled applications.
 extra-source-files: CHANGELOG.md, README.md
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crucible-llvm
+
 common bldflags
   ghc-options: -Wall
                -Werror=incomplete-patterns
diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
index e992d521c..e463735a7 100644
--- a/crucible-symio/crucible-symio.cabal
+++ b/crucible-symio/crucible-symio.cabal
@@ -13,6 +13,11 @@ maintainer:          dmatichuk@galois.com
 build-type:          Simple
 extra-source-files:  CHANGELOG.md
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crucible-symio
+
 common shared
   build-depends:       base >=4.12 && <4.19,
                        aeson,
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index 8e0201d24..36fe11883 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -16,6 +16,11 @@ Description:
   a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.
 extra-source-files: CHANGELOG.md
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crucible
+
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
 -- to False, alternate implementations are used to avoid
diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 44354cde5..59458a933 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -41,6 +41,11 @@ data-files:
    c-src/libcxx-7.1.0.bc
 extra-source-files: CHANGELOG.md, README.md
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crux-llvm
+
 common bldflags
   ghc-options: -Wall
                -Werror=incomplete-patterns
diff --git a/crux/crux.cabal b/crux/crux.cabal
index 60d1d3fea..07dac046c 100644
--- a/crux/crux.cabal
+++ b/crux/crux.cabal
@@ -17,6 +17,11 @@ Description:
   verification, usually by embedding verification specifications in
   the source language.
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crux
+
 library
 
   build-depends:

From 8646abdae57cc67d1f73d15a37e3fe18260f22bc Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:11:15 -0500
Subject: [PATCH 18/32] crucible-symio.cabal: Fill in missing category and
 license fields

(cherry picked from commit 2c9747c8cd71fd5816ebd56a8ed109e781e4f66f)
---
 crucible-symio/crucible-symio.cabal | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
index e463735a7..8d3a87286 100644
--- a/crucible-symio/crucible-symio.cabal
+++ b/crucible-symio/crucible-symio.cabal
@@ -7,10 +7,12 @@ description:
   programs that e.g., use configuration files or accept input from files.
 name:                crucible-symio
 version:             0.1.0.0
+license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Daniel Matichuk
 maintainer:          dmatichuk@galois.com
 build-type:          Simple
+category:            Language
 extra-source-files:  CHANGELOG.md
 
 source-repository head

From 1c1e7de205d92846f1974c95517a4d60e2d8e77a Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:16:03 -0500
Subject: [PATCH 19/32] crucible{,-llvm}.cabal: Use -fprof-top-exported, not
 -fprof-top-auto

Annoyingly, `cabal check` will reject your `.cabal` file if it enabled
`-fprof-top-auto`, instead suggesting `-fprof-top-exported` as a blessed
alternative. I don't quite agree with this suggestion, but it is the most
direct way to make Hackage accept these `.cabal` files.

(cherry picked from commit 25e7b3a134ab8ca77cc989717957dab86d1ba0b5)
---
 crucible-llvm/crucible-llvm.cabal | 2 +-
 crucible/crucible.cabal           | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index 1913ba973..b4d045a6d 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -26,7 +26,7 @@ common bldflags
                -Werror=overlapping-patterns
                -Wpartial-fields
                -Wincomplete-uni-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -O2 -fprof-auto-exported
   default-language: Haskell2010
 
 
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index 36fe11883..02cf0c1f5 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -37,7 +37,7 @@ common bldflags
                -Werror=overlapping-patterns
                -Wpartial-fields
                -Wincomplete-uni-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -O2 -fprof-auto-exported
   default-language: Haskell2010
 
 

From 207371fef1413e39d897449e9f9b8ee148b51ed9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Mon, 5 Feb 2024 07:53:40 -0500
Subject: [PATCH 20/32] crucible-llvm: Require llvm-pretty >= 0.12 && < 0.13

(cherry picked from commit 981c36a18f150d6473693abb5b9a9559e01809a3)
---
 crucible-llvm/crucible-llvm.cabal | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index b4d045a6d..cbb949df5 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -44,7 +44,7 @@ library
     extra,
     lens,
     itanium-abi >= 0.1.1.1 && < 0.2,
-    llvm-pretty >= 0.8 && < 0.12,
+    llvm-pretty >= 0.12 && < 0.13,
     mtl,
     parameterized-utils >= 2.1.5 && < 2.2,
     pretty,

From 9df8c3f9ae09b468c165307ff545f50197b6dd15 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 5 Feb 2024 09:40:12 -0500
Subject: [PATCH 21/32] Bump llvm-pretty, llvm-pretty-bc-parser submodules

(cherry picked from commit c0e6fb1f67dbcba091061d22282a2f659be9c064)
---
 dependencies/llvm-pretty           | 2 +-
 dependencies/llvm-pretty-bc-parser | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/dependencies/llvm-pretty b/dependencies/llvm-pretty
index 8124fc026..780e7c01c 160000
--- a/dependencies/llvm-pretty
+++ b/dependencies/llvm-pretty
@@ -1 +1 @@
-Subproject commit 8124fc0265b6ca5fde5812c789f40b2ea54af678
+Subproject commit 780e7c01cbd0b85172f11ea8edf0d7bbe6a84967
diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser
index 39b4a5ff2..395754789 160000
--- a/dependencies/llvm-pretty-bc-parser
+++ b/dependencies/llvm-pretty-bc-parser
@@ -1 +1 @@
-Subproject commit 39b4a5ff26ad88f7db250185cc5b471fac50141d
+Subproject commit 395754789b2f1b1f3ffae22383f9522a3e44d68e

From e2aa0e070cd4a794c40b2cb18c530794620c4b83 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 5 Feb 2024 09:19:11 -0500
Subject: [PATCH 22/32] CI: Regenerate cabal.GHC-*.config files

(cherry picked from commit 4e0ef8cd68a840c973668891ca53bb801aee3daa)
---
 cabal.GHC-8.10.7.config | 12 ++++++------
 cabal.GHC-9.2.8.config  | 12 ++++++------
 cabal.GHC-9.4.5.config  | 12 ++++++------
 cabal.GHC-9.6.2.config  | 12 ++++++------
 4 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config
index 68cd86be5..36f883f3c 100644
--- a/cabal.GHC-8.10.7.config
+++ b/cabal.GHC-8.10.7.config
@@ -26,7 +26,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.14.3.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.1,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config
index e63dbfb3b..0908e7658 100644
--- a/cabal.GHC-9.2.8.config
+++ b/cabal.GHC-9.2.8.config
@@ -26,7 +26,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.16.4.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.4.5.config b/cabal.GHC-9.4.5.config
index 68a2e610d..cbf2fbe08 100644
--- a/cabal.GHC-9.4.5.config
+++ b/cabal.GHC-9.4.5.config
@@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.17.1.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.6.2.config b/cabal.GHC-9.6.2.config
index b3fb185de..96a402649 100644
--- a/cabal.GHC-9.6.2.config
+++ b/cabal.GHC-9.6.2.config
@@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.18.0.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -177,7 +177,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -189,7 +189,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -209,7 +209,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -269,7 +269,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -284,4 +284,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z

From 1fadd88abad4de15ea30eb1ba643967e3c3bce1b Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:19:26 -0500
Subject: [PATCH 23/32] Update maintainers for crux-llvm and its dependencies

(cherry picked from commit db01e4bdad525a275df243fe3035f8522bb65a5d)
---
 crucible-llvm/crucible-llvm.cabal   | 2 +-
 crucible-symio/crucible-symio.cabal | 2 +-
 crucible/crucible.cabal             | 2 +-
 crux-llvm/crux-llvm.cabal           | 2 +-
 crux/crux.cabal                     | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index cbb949df5..5ae88ea75 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -3,7 +3,7 @@ Name:          crucible-llvm
 Version:       0.5
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2022
-Maintainer:    rdockins@galois.com
+Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 License:       BSD-3-Clause
 License-file:  LICENSE
 Build-type:    Simple
diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
index 8d3a87286..d63b6685f 100644
--- a/crucible-symio/crucible-symio.cabal
+++ b/crucible-symio/crucible-symio.cabal
@@ -10,7 +10,7 @@ version:             0.1.0.0
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Daniel Matichuk
-maintainer:          dmatichuk@galois.com
+maintainer:          rscott@galois.com, kquick@galois.com, langston@galois.com
 build-type:          Simple
 category:            Language
 extra-source-files:  CHANGELOG.md
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index 02cf0c1f5..0aa138617 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -2,7 +2,7 @@ Cabal-version: 2.2
 Name:          crucible
 Version:       0.6
 Author:        Galois Inc.
-Maintainer:    jhendrix@galois.com, rdockins@galois.com
+Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
 License:       BSD-3-Clause
 License-file:  LICENSE
diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 59458a933..77d1ab382 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -2,7 +2,7 @@ Cabal-version: 2.2
 Name:          crux-llvm
 Version:       0.7.0.99
 Author:        Galois Inc.
-Maintainer:    iavor.diatchki@gmail.com
+Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
 License:       BSD-3-Clause
 License-file:  LICENSE
diff --git a/crux/crux.cabal b/crux/crux.cabal
index 07dac046c..4e8bf0636 100644
--- a/crux/crux.cabal
+++ b/crux/crux.cabal
@@ -3,7 +3,7 @@ Name:          crux
 Version:       0.6.0.99
 Copyright:     (c) Galois, Inc. 2018-2022
 Author:        sweirich@galois.com
-Maintainer:    rdockins@galois.com
+Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 License:       BSD-3-Clause
 License-file:  LICENSE
 Build-type:    Simple

From efda469a2eb937cbf5a359f42e345b03cf78edf9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:25:55 -0500
Subject: [PATCH 24/32] Mention #1162 in the crux-llvm CHANGELOG

(cherry picked from commit d8fba04b519850834a0b044a7fcd1a4000804c3d)
---
 crux-llvm/CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
index 90d201578..15b87a468 100644
--- a/crux-llvm/CHANGELOG.md
+++ b/crux-llvm/CHANGELOG.md
@@ -1,3 +1,7 @@
+# next
+
+* Add support for LLVM bitcode files generated by Apple Clang on macOS.
+
 # 0.7 -- 2023-06-26
 
 ## New features

From dde5febfe3a635d800ae0ae59d2cdf6dceace2ea Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:31:15 -0500
Subject: [PATCH 25/32] Use 0.1, not 0.1.0.0, to match version conventions
 elsewhere

(cherry picked from commit 93e8f8db0458dc4384f48f0c7dd5daa0f30b8c8a)
---
 crucible-concurrency/crucible-concurrency.cabal | 2 +-
 crucible-go/crucible-go.cabal                   | 2 +-
 crucible-symio/CHANGELOG.md                     | 2 +-
 crucible-symio/crucible-symio.cabal             | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/crucible-concurrency/crucible-concurrency.cabal b/crucible-concurrency/crucible-concurrency.cabal
index 738e82783..1f4e07031 100644
--- a/crucible-concurrency/crucible-concurrency.cabal
+++ b/crucible-concurrency/crucible-concurrency.cabal
@@ -3,7 +3,7 @@ cabal-version:       2.4
 --   For further documentation, see http://haskell.org/cabal/users-guide/
 
 name:                crucible-concurrency
-version:             0.1.0.0
+version:             0.1
 -- synopsis:
 -- description:
 -- bug-reports:
diff --git a/crucible-go/crucible-go.cabal b/crucible-go/crucible-go.cabal
index c3080e797..60b075f72 100644
--- a/crucible-go/crucible-go.cabal
+++ b/crucible-go/crucible-go.cabal
@@ -1,5 +1,5 @@
 name:                crucible-go
-version:             0.1.0.0
+version:             0.1
 synopsis:            A Go frontend for Crucible
 license:             BSD3
 license-file:        LICENSE
diff --git a/crucible-symio/CHANGELOG.md b/crucible-symio/CHANGELOG.md
index cff4521b6..b9a04fde6 100644
--- a/crucible-symio/CHANGELOG.md
+++ b/crucible-symio/CHANGELOG.md
@@ -1,5 +1,5 @@
 # Revision history for crucible-symio
 
-## 0.1.0.0 -- YYYY-mm-dd
+## 0.1 -- YYYY-mm-dd
 
 * First version. Released on an unsuspecting world.
diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
index d63b6685f..52de4761d 100644
--- a/crucible-symio/crucible-symio.cabal
+++ b/crucible-symio/crucible-symio.cabal
@@ -6,7 +6,7 @@ description:
   reading and writing symbolic data. An example use case would be to support verifying
   programs that e.g., use configuration files or accept input from files.
 name:                crucible-symio
-version:             0.1.0.0
+version:             0.1
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Daniel Matichuk

From 0f8db147f8bd7ab111d34e46c739771a94011fa0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:34:45 -0500
Subject: [PATCH 26/32] Update CHANGELOGs in preparation for releases

(cherry picked from commit 529b365a2190d04d95247316829271db08465ff7)
---
 crucible-cli/CHANGELOG.md         | 4 ++--
 crucible-go/CHANGELOG.md          | 2 +-
 crucible-jvm/CHANGELOG.md         | 2 +-
 crucible-llvm-cli/CHANGELOG.md    | 4 ++--
 crucible-llvm-syntax/CHANGELOG.md | 4 ++--
 crucible-llvm/CHANGELOG.md        | 2 +-
 crucible-mir/CHANGELOG.md         | 2 +-
 crucible-syntax/CHANGELOG.md      | 2 +-
 crucible/CHANGELOG.md             | 3 +++
 crux-llvm/CHANGELOG.md            | 2 +-
 crux-mir/CHANGELOG.md             | 2 +-
 crux/CHANGELOG.md                 | 2 +-
 12 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md
index 956a58949..28245fa54 100644
--- a/crucible-cli/CHANGELOG.md
+++ b/crucible-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# next
+# 0.1
 
-* TODO: Describe API changes here
+* Initial version. Split off from `crucible-syntax`.
diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md
index 512f2eb05..15e4e8d96 100644
--- a/crucible-go/CHANGELOG.md
+++ b/crucible-go/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.1
 
 * Change `SomeOverride`, as well as related functions in
   `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`.
diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md
index 36dc6c410..3c0441688 100644
--- a/crucible-jvm/CHANGELOG.md
+++ b/crucible-jvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.2
 
 * Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a
   `TypedOverride`.
diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md
index 956a58949..9e46ac60c 100644
--- a/crucible-llvm-cli/CHANGELOG.md
+++ b/crucible-llvm-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# next
+# 0.1
 
-* TODO: Describe API changes here
+* Initial version.
diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md
index 956a58949..9e46ac60c 100644
--- a/crucible-llvm-syntax/CHANGELOG.md
+++ b/crucible-llvm-syntax/CHANGELOG.md
@@ -1,3 +1,3 @@
-# next
+# 0.1
 
-* TODO: Describe API changes here
+* Initial version.
diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index 9129b111f..e57bfaef1 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.6
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.
   Use `decName` to get a `Symbol` from a `Declare`.
diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 933a08925..20bceace0 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.2
 
 * `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of
   the highlights of this include:
diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md
index 4bb8af8ce..0732e8b42 100644
--- a/crucible-syntax/CHANGELOG.md
+++ b/crucible-syntax/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.4
 
 * The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,
   which serves a similar purpose (hiding the argument and return types). The
diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
index 947281966..fb70e0860 100644
--- a/crucible/CHANGELOG.md
+++ b/crucible/CHANGELOG.md
@@ -2,6 +2,9 @@
 
 * Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`,
   provide helpers such as `popFrame` to manage assumptions without `panic`ing.
+
+# 0.7
+
 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to
   `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an
   `OverrideSim` action and bundle `TypeRepr`s for its argument and result
diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
index 15b87a468..c9fc1d151 100644
--- a/crux-llvm/CHANGELOG.md
+++ b/crux-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.8
 
 * Add support for LLVM bitcode files generated by Apple Clang on macOS.
 
diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index 3d68c9b91..acf1e1439 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.8
 
 * `crux-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of the
    highlights of this include:
diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
index dcf53179b..ca317ea8e 100644
--- a/crux/CHANGELOG.md
+++ b/crux/CHANGELOG.md
@@ -1,4 +1,4 @@
-# next
+# 0.7
 
 * Add a `Crux.Overrides` module, which defines common functionality for defining
   overrides, which are shared among several Crux backends.

From 193d63903a510e6a17b629ab7ca9e1f8602720aa Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 31 Jan 2024 16:38:30 -0500
Subject: [PATCH 27/32] Release dates for CHANGELOGs

(cherry picked from commit e1b34f501622060375a8d0ad44605629ab96210d)
---
 crucible-cli/CHANGELOG.md         | 2 +-
 crucible-go/CHANGELOG.md          | 2 +-
 crucible-jvm/CHANGELOG.md         | 2 +-
 crucible-llvm-cli/CHANGELOG.md    | 2 +-
 crucible-llvm-syntax/CHANGELOG.md | 2 +-
 crucible-llvm/CHANGELOG.md        | 2 +-
 crucible-mir/CHANGELOG.md         | 2 +-
 crucible-symio/CHANGELOG.md       | 2 +-
 crucible-syntax/CHANGELOG.md      | 2 +-
 crucible/CHANGELOG.md             | 4 ++--
 crux-llvm/CHANGELOG.md            | 2 +-
 crux-mir/CHANGELOG.md             | 2 +-
 crux/CHANGELOG.md                 | 2 +-
 13 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md
index 28245fa54..8b657180c 100644
--- a/crucible-cli/CHANGELOG.md
+++ b/crucible-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1
+# 0.1 -- 2024-??-??
 
 * Initial version. Split off from `crucible-syntax`.
diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md
index 15e4e8d96..5d76eb7be 100644
--- a/crucible-go/CHANGELOG.md
+++ b/crucible-go/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.1
+# 0.1 -- 2024-??-??
 
 * Change `SomeOverride`, as well as related functions in
   `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`.
diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md
index 3c0441688..d05d71620 100644
--- a/crucible-jvm/CHANGELOG.md
+++ b/crucible-jvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.2
+# 0.2 -- 2024-??-??
 
 * Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a
   `TypedOverride`.
diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md
index 9e46ac60c..903a4832c 100644
--- a/crucible-llvm-cli/CHANGELOG.md
+++ b/crucible-llvm-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1
+# 0.1 -- 2024-??-??
 
 * Initial version.
diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md
index 9e46ac60c..903a4832c 100644
--- a/crucible-llvm-syntax/CHANGELOG.md
+++ b/crucible-llvm-syntax/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1
+# 0.1 -- 2024-??-??
 
 * Initial version.
diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index e57bfaef1..f39fd51d6 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.6
+# 0.6 -- 2024-??-??
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.
   Use `decName` to get a `Symbol` from a `Declare`.
diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 20bceace0..a2f1499b6 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.2
+# 0.2 -- 2024-??-??
 
 * `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of
   the highlights of this include:
diff --git a/crucible-symio/CHANGELOG.md b/crucible-symio/CHANGELOG.md
index b9a04fde6..e5737b689 100644
--- a/crucible-symio/CHANGELOG.md
+++ b/crucible-symio/CHANGELOG.md
@@ -1,5 +1,5 @@
 # Revision history for crucible-symio
 
-## 0.1 -- YYYY-mm-dd
+## 0.1 -- 2024-??-??
 
 * First version. Released on an unsuspecting world.
diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md
index 0732e8b42..7f9d1aa5a 100644
--- a/crucible-syntax/CHANGELOG.md
+++ b/crucible-syntax/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.4
+# 0.4 -- 2024-??-??
 
 * The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,
   which serves a similar purpose (hiding the argument and return types). The
diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
index fb70e0860..9da2ee317 100644
--- a/crucible/CHANGELOG.md
+++ b/crucible/CHANGELOG.md
@@ -1,9 +1,9 @@
-# next
+# next -- TBA
 
 * Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`,
   provide helpers such as `popFrame` to manage assumptions without `panic`ing.
 
-# 0.7
+# 0.7 -- 2024-??-??
 
 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to
   `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an
diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
index c9fc1d151..e27fb3403 100644
--- a/crux-llvm/CHANGELOG.md
+++ b/crux-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.8
+# 0.8 -- 2024-??-??
 
 * Add support for LLVM bitcode files generated by Apple Clang on macOS.
 
diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index acf1e1439..3d0e6ec5c 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.8
+# 0.8 -- 2024-??-??
 
 * `crux-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of the
    highlights of this include:
diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
index ca317ea8e..9875b2988 100644
--- a/crux/CHANGELOG.md
+++ b/crux/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.7
+# 0.7 -- 2024-??-??
 
 * Add a `Crux.Overrides` module, which defines common functionality for defining
   overrides, which are shared among several Crux backends.

From ed10449195b75463eca067b3a6257aaf03829291 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 1 Feb 2024 11:49:33 -0500
Subject: [PATCH 28/32] Bump release versions for Crux 0.8 series

This bumps `crux-{llvm,mir}` to version `0.8`, and it also bumps the release
versions of other libraries that are destined for Hackage or have otherwise
seen significant API changes.

(cherry picked from commit e49efb25736c5f03a6dd2193a55e657db27e25ef)
---
 crucible-llvm/crucible-llvm.cabal     | 2 +-
 crucible-mir/crucible-mir.cabal       | 2 +-
 crucible-syntax/crucible-syntax.cabal | 2 +-
 crucible/crucible.cabal               | 2 +-
 crux-llvm/crux-llvm.cabal             | 2 +-
 crux-mir/crux-mir.cabal               | 2 +-
 crux/crux.cabal                       | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index 5ae88ea75..26b3f93c4 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible-llvm
-Version:       0.5
+Version:       0.6
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2022
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
diff --git a/crucible-mir/crucible-mir.cabal b/crucible-mir/crucible-mir.cabal
index c5846ce1d..ab459807f 100644
--- a/crucible-mir/crucible-mir.cabal
+++ b/crucible-mir/crucible-mir.cabal
@@ -1,5 +1,5 @@
 name:                crucible-mir
-version:             0.1
+version:             0.2
 -- synopsis:
 -- description:
 homepage:            https://github.com/GaloisInc/crucible/blob/master/crucible-mir/README.md
diff --git a/crucible-syntax/crucible-syntax.cabal b/crucible-syntax/crucible-syntax.cabal
index 2839dba14..3f6c14cad 100644
--- a/crucible-syntax/crucible-syntax.cabal
+++ b/crucible-syntax/crucible-syntax.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible-syntax
-Version:       0.3
+Version:       0.4
 Author:        Galois Inc.
 Maintainer:    dtc@galois.com
 Build-type:    Simple
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index 0aa138617..ba771a4c3 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible
-Version:       0.6
+Version:       0.7
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 77d1ab382..7d44c29f7 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux-llvm
-Version:       0.7.0.99
+Version:       0.8
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
diff --git a/crux-mir/crux-mir.cabal b/crux-mir/crux-mir.cabal
index efabd85b3..c23fee943 100644
--- a/crux-mir/crux-mir.cabal
+++ b/crux-mir/crux-mir.cabal
@@ -1,5 +1,5 @@
 name:                crux-mir
-version:             0.7.0.99
+version:             0.8
 -- synopsis:
 -- description:
 homepage:            https://github.com/GaloisInc/crucible/blob/master/crux-mir/README.md
diff --git a/crux/crux.cabal b/crux/crux.cabal
index 4e8bf0636..bb880823a 100644
--- a/crux/crux.cabal
+++ b/crux/crux.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux
-Version:       0.6.0.99
+Version:       0.7
 Copyright:     (c) Galois, Inc. 2018-2022
 Author:        sweirich@galois.com
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com

From c74172f368af218fa9852cb7b9ac7ae9f6b00368 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 5 Feb 2024 15:03:07 -0500
Subject: [PATCH 29/32] Finalize Crux 0.8 dates

(cherry picked from commit 9a5d6cc32c8351722ab8b489a634b78f62337805)
---
 crucible-cli/CHANGELOG.md         | 2 +-
 crucible-go/CHANGELOG.md          | 2 +-
 crucible-jvm/CHANGELOG.md         | 2 +-
 crucible-llvm-cli/CHANGELOG.md    | 2 +-
 crucible-llvm-syntax/CHANGELOG.md | 2 +-
 crucible-llvm/CHANGELOG.md        | 2 +-
 crucible-mir/CHANGELOG.md         | 2 +-
 crucible-symio/CHANGELOG.md       | 2 +-
 crucible-syntax/CHANGELOG.md      | 2 +-
 crucible/CHANGELOG.md             | 2 +-
 crux-llvm/CHANGELOG.md            | 2 +-
 crux-mir/CHANGELOG.md             | 2 +-
 crux/CHANGELOG.md                 | 2 +-
 13 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md
index 8b657180c..362245e3b 100644
--- a/crucible-cli/CHANGELOG.md
+++ b/crucible-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1 -- 2024-??-??
+# 0.1 -- 2024-02-05
 
 * Initial version. Split off from `crucible-syntax`.
diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md
index 5d76eb7be..95d60e2fd 100644
--- a/crucible-go/CHANGELOG.md
+++ b/crucible-go/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.1 -- 2024-??-??
+# 0.1 -- 2024-02-05
 
 * Change `SomeOverride`, as well as related functions in
   `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`.
diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md
index d05d71620..b102740ad 100644
--- a/crucible-jvm/CHANGELOG.md
+++ b/crucible-jvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.2 -- 2024-??-??
+# 0.2 -- 2024-02-05
 
 * Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a
   `TypedOverride`.
diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md
index 903a4832c..688e82de1 100644
--- a/crucible-llvm-cli/CHANGELOG.md
+++ b/crucible-llvm-cli/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1 -- 2024-??-??
+# 0.1 -- 2024-02-05
 
 * Initial version.
diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md
index 903a4832c..688e82de1 100644
--- a/crucible-llvm-syntax/CHANGELOG.md
+++ b/crucible-llvm-syntax/CHANGELOG.md
@@ -1,3 +1,3 @@
-# 0.1 -- 2024-??-??
+# 0.1 -- 2024-02-05
 
 * Initial version.
diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
index f39fd51d6..76d070fe7 100644
--- a/crucible-llvm/CHANGELOG.md
+++ b/crucible-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.6 -- 2024-??-??
+# 0.6 -- 2024-02-05
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.
   Use `decName` to get a `Symbol` from a `Declare`.
diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index a2f1499b6..0e5085815 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.2 -- 2024-??-??
+# 0.2 -- 2024-02-05
 
 * `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of
   the highlights of this include:
diff --git a/crucible-symio/CHANGELOG.md b/crucible-symio/CHANGELOG.md
index e5737b689..5c1073d8e 100644
--- a/crucible-symio/CHANGELOG.md
+++ b/crucible-symio/CHANGELOG.md
@@ -1,5 +1,5 @@
 # Revision history for crucible-symio
 
-## 0.1 -- 2024-??-??
+## 0.1 -- 2024-02-05
 
 * First version. Released on an unsuspecting world.
diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md
index 7f9d1aa5a..4ce9021cc 100644
--- a/crucible-syntax/CHANGELOG.md
+++ b/crucible-syntax/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.4 -- 2024-??-??
+# 0.4 -- 2024-02-05
 
 * The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,
   which serves a similar purpose (hiding the argument and return types). The
diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
index 9da2ee317..8a502f7ef 100644
--- a/crucible/CHANGELOG.md
+++ b/crucible/CHANGELOG.md
@@ -3,7 +3,7 @@
 * Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`,
   provide helpers such as `popFrame` to manage assumptions without `panic`ing.
 
-# 0.7 -- 2024-??-??
+# 0.7 -- 2024-02-05
 
 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to
   `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an
diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
index e27fb3403..85da156ba 100644
--- a/crux-llvm/CHANGELOG.md
+++ b/crux-llvm/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.8 -- 2024-??-??
+# 0.8 -- 2024-02-05
 
 * Add support for LLVM bitcode files generated by Apple Clang on macOS.
 
diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index 3d0e6ec5c..0e83e1715 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.8 -- 2024-??-??
+# 0.8 -- 2024-02-05
 
 * `crux-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of the
    highlights of this include:
diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
index 9875b2988..cd505f4c2 100644
--- a/crux/CHANGELOG.md
+++ b/crux/CHANGELOG.md
@@ -1,4 +1,4 @@
-# 0.7 -- 2024-??-??
+# 0.7 -- 2024-02-05
 
 * Add a `Crux.Overrides` module, which defines common functionality for defining
   overrides, which are shared among several Crux backends.

From 0ece69752b81e3fd0c3fddb9c76843824f1369b0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 5 Feb 2024 15:17:51 -0500
Subject: [PATCH 30/32] CI: Properly detect when releases are tagged

(cherry picked from commit e4e532ff95768059f808a351253108c5d62e7c99)
---
 .github/workflows/crux-llvm-build.yml | 4 ++--
 .github/workflows/crux-mir-build.yml  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
index 724317f46..87cc4fb7d 100644
--- a/.github/workflows/crux-llvm-build.yml
+++ b/.github/workflows/crux-llvm-build.yml
@@ -31,7 +31,7 @@ jobs:
       event-tag: ${{ steps.config.outputs.tag }}
       event-schedule: ${{ steps.config.outputs.schedule }}
       publish: ${{ steps.config.outputs.publish }}
-      release: ${{ steps.env.outputs.release }}
+      release: ${{ steps.config.outputs.release }}
       retention-days: ${{ steps.config.outputs.retention-days }}
     steps:
       - uses: actions/checkout@v2
@@ -52,7 +52,7 @@ jobs:
           .github/ci.sh output tag $EVENT_TAG
           .github/ci.sh output schedule $EVENT_SCHEDULE
           .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false)
-          .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
+          .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
           .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
 
   build:
diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml
index 235b1c8ab..e7ab9feda 100644
--- a/.github/workflows/crux-mir-build.yml
+++ b/.github/workflows/crux-mir-build.yml
@@ -33,7 +33,7 @@ jobs:
       event-tag: ${{ steps.config.outputs.tag }}
       event-schedule: ${{ steps.config.outputs.schedule }}
       publish: ${{ steps.config.outputs.publish }}
-      release: ${{ steps.env.outputs.release }}
+      release: ${{ steps.config.outputs.release }}
       retention-days: ${{ steps.config.outputs.retention-days }}
     steps:
       - uses: actions/checkout@v2
@@ -54,7 +54,7 @@ jobs:
           .github/ci.sh output tag $EVENT_TAG
           .github/ci.sh output schedule $EVENT_SCHEDULE
           .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false)
-          .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
+          .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
           .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
 
   build:

From 71227de226feabee74bbd4f6cf53c4f888a3b2e0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 5 Feb 2024 16:27:19 -0500
Subject: [PATCH 31/32] CI: Use correct Docker image tag

(cherry picked from commit e40589e86a0604d2d117f53430923f9aa4fa732c)
---
 .github/workflows/crux-llvm-build.yml | 6 +++---
 .github/workflows/crux-mir-build.yml  | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
index 87cc4fb7d..ea6149e76 100644
--- a/.github/workflows/crux-llvm-build.yml
+++ b/.github/workflows/crux-llvm-build.yml
@@ -369,9 +369,9 @@ jobs:
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
-        name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
+        name: ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
+          docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
           docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest
diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml
index e7ab9feda..62bd7fdf7 100644
--- a/.github/workflows/crux-mir-build.yml
+++ b/.github/workflows/crux-mir-build.yml
@@ -276,9 +276,9 @@ jobs:
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
-        name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
+        name: ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
+          docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
           docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest

From 3633bd72938e56679e7fdfa9286eea86e648620a Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 1 Feb 2024 11:51:56 -0500
Subject: [PATCH 32/32] Bump development versions for Crux and related
 libraries

This bumps the development versions of `crux-{llvm,mir}` to `0.8.0.0.99`, as
well as the development versions of other libraries that are uploaded to
Hackage.
---
 crucible-llvm/crucible-llvm.cabal   | 2 +-
 crucible-symio/crucible-symio.cabal | 2 +-
 crucible/crucible.cabal             | 2 +-
 crux-llvm/crux-llvm.cabal           | 2 +-
 crux-mir/crux-mir.cabal             | 2 +-
 crux/crux.cabal                     | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
index 26b3f93c4..6b3c24b5f 100644
--- a/crucible-llvm/crucible-llvm.cabal
+++ b/crucible-llvm/crucible-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible-llvm
-Version:       0.6
+Version:       0.6.0.99
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2022
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
index 52de4761d..12602db01 100644
--- a/crucible-symio/crucible-symio.cabal
+++ b/crucible-symio/crucible-symio.cabal
@@ -6,7 +6,7 @@ description:
   reading and writing symbolic data. An example use case would be to support verifying
   programs that e.g., use configuration files or accept input from files.
 name:                crucible-symio
-version:             0.1
+version:             0.1.0.99
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Daniel Matichuk
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index ba771a4c3..d1f853645 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible
-Version:       0.7
+Version:       0.7.0.99
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 7d44c29f7..91d3cc35d 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux-llvm
-Version:       0.8
+Version:       0.8.0.99
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
diff --git a/crux-mir/crux-mir.cabal b/crux-mir/crux-mir.cabal
index c23fee943..31d9245f1 100644
--- a/crux-mir/crux-mir.cabal
+++ b/crux-mir/crux-mir.cabal
@@ -1,5 +1,5 @@
 name:                crux-mir
-version:             0.8
+version:             0.8.0.99
 -- synopsis:
 -- description:
 homepage:            https://github.com/GaloisInc/crucible/blob/master/crux-mir/README.md
diff --git a/crux/crux.cabal b/crux/crux.cabal
index bb880823a..eeceb3036 100644
--- a/crux/crux.cabal
+++ b/crux/crux.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux
-Version:       0.7
+Version:       0.7.0.99
 Copyright:     (c) Galois, Inc. 2018-2022
 Author:        sweirich@galois.com
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com