crucible-0.10: CHANGELOG.md

# 0.10 -- 2026-09-10

* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.
* Fix `uniquelyConcRegMap` blocking clause: use disjunction (OR) instead of
  conjunction (AND). The old code would falsely report a `RegMap` as uniquely
  concretized whenever any single component was unique, even if other components
  had multiple possible values.
* **BREAKING:** Rename various bits associated with the "breakpoint"
  feature in accordance with renaming the feature to "cut" or
  "cutpoint".
  Exported Haskell symbols renamed:
  - `Lang.Crucible.Simulator.Breakpoint` -> `Lang.Crucible.Simulator.Cut`
  - `BreakpointName` -> `CutpointName`
  - `Breakpoint` -> `Cut`
  - `addBreakpointStmt` -> `addCutStmt`
  - `breakAndReturn` -> `cutAndReturn`
  - `breakpointPostdomInfo` -> `cutpointPostdomInfo`
  - `cfgBreakpoints` -> `cfgCutpoints`
  - `setFrameBreakpointPostdomInfo` -> `setFrameCutpointPostdomInfo`
* Add `reverseSymSequence` to `Lang.Crucible.Simulator.SymSequence`
* **BREAKING:** Add `FloatRound` constructor tp `App` in
  `Lang.Crucible.CFG.Expr` for rounding floating-point values to the nearest
  representable integral value.
* **BREAKING:** Add `SequenceReverse` constructor to `App` in
  `Lang.Crucible.CFG.Expr` for reversing symbolic sequences.
* **BREAKING:** Change the signature of `getRecordedTrace` in
  `Lang.Crucible.Simulator.RecordAndReplay` to remove the `evalBool` parameter,
  as the implementation no longer concretizes the trace.
* Add `Lang.Crucible.Simulator.RecordAndReplay.getConcreteRecordedTrace` for
  performant trace reversal when concretization is desired.
* Add `withStateBackend` and additional infrastructure for including stack
  traces in `SimError` and `IsSymBackend`
* Fix `onlineProve` to properly negate goals before checking satisfiability
* Avoid sending trivially-true goals to the solver in `Backend.Prove`.
* Fix bug in `execResultGlobals` that caused it to erroneously always return the
  non-aborted branch of a `FinishedResult ... (PartialRes ...)`.

# 0.9 -- 2026-01-29

# 0.8.0 -- 2025-11-09

* Add `setExecResultContext`, `setExecStateContext`
* Add `Lang.Crucible.Simulator.RecordAndReplay`, a module with two new execution
  features for recording and replaying control-flow traces.
* Add a `GlobalPair` argument to `AbortedExit`.
* Add new helpers for extracting `SymGlobalState`s: `exec{Result,State}Globals`.
* Add `typedOverride` for constructing `TypedOverride`s with statically-known
  signatures.
* Add `bindTypedOverride` for binding `TypedOverride`s to `FnHandle`s.
* Add `FunctorF`, `FoldableF`, and `TraversableF` instances for `CrucibleEvent`,
  `CrucibleAssumption`, and `CrucibleAssumptions`.
* Add `gcAddTopLevelAssume`, for making top-level assumptions.
* Rename functions in `Lang.Crucible.Concretize` to match What4's conventions.
  In particular, rename  `concRegValue` to `groundRegValue`, `concRegEntry` to
  `groundRegEntry`, and `concRegMap` to `groundRegMap`.

# 0.7.2 -- 2025-03-21

* Add support for Bitwuzla as an online SMT solver backend.
* Add a function `ppTypeRepr` to `Lang.Crucible.Types` for pretty-printing
  `TypeRepr`s. Modify the `Pretty` instance to use this function.
* Add an `EqF TypeRepr` instance.

# 0.7.1 -- 2024-08-30

* Add support for GHC 9.8

* Deprecate `concreteizeSymSequence` in favor of `concretizeSymSequence`

# 0.7 -- 2024-02-05

* 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.
* Add `Lang.Crucible.Simulator.OverrideSim.bindCFG`, a utility function for
  binding a CFG to its handle in an `OverrideSim`.

# 0.6

* Separate backend data structures.  The "symbolic backend" is a
ubiquitous datatype throughout Crucible. Previously, this single
data structure was responsible for symbolic expression creation
and also for tracking the structure of assumptions and assertions
as the symbolic simulator progresses. These linked purposes made
certain code patterns very difficult, such as running related symbolic
simulation instances in separate threads, or configuring different
online solvers for path satisfiability checking.

We changed this structure so that the `sym` value is now only
responsible for the What4 expression creation tasks.  Now, there is a
new "symbolic backend" `bak` value (that contains a `sym`) which is
used to handle path conditions and assertions.  These two values are
connected by the `IsSymBackend sym bak` type class.  To prevent even
more code churn than is already occurring, the exact type of `bak` is
wrapped up into an existential datatype and stored in the
`SimContext`. This makes accessing the symbolic backend a little less
convenient, but prevents the new type from leaking into every type
signature that currently mentions `sym`.  The `withBackend`
and `ovrWithBackend` operations (written in a CPS style) are the
easiest way to get access to the backend, but it can also be accessed
via directly pattern matching on the existential `SomeBackend` type.

For many purposes the old `sym` value is still sufficient, and the
`bak` value is not necessary. A good rule is that any operation
that adds assumptions or assertions to the context will need
the full symbolic backend `bak`, but any operation that just
builds terms will only need the `sym`.