Skip to content

Conversation

RyanGlScott
Copy link
Contributor

Doing so is necessary to work around a bug in the implementation of IntMap.mergeWithKey that exists in pre-0.8 versions of the containers library (haskell/containers#979), which all currently supported versions of GHC currently use. See the newly added comments in traverseMirAggregate for the full story.

Fixes #2687.

@RyanGlScott RyanGlScott self-assigned this Oct 7, 2025
@RyanGlScott RyanGlScott added the subsystem: crucible-mir-comp Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp label Oct 7, 2025
Doing so is necessary to work around a bug in the implementation of
`IntMap.mergeWithKey` that exists in pre-0.8 versions of the `containers`
library (haskell/containers#979), which all currently
supported versions of GHC currently use. See the newly added comments in
`traverseMirAggregate` for the full story.

Fixes #2687.
@RyanGlScott RyanGlScott force-pushed the T2687-fix-traverseMirAggregate-bug branch from 1a1c5aa to fe303c4 Compare October 7, 2025 22:52
@RyanGlScott RyanGlScott merged commit a7855cf into master Oct 8, 2025
37 checks passed
@RyanGlScott RyanGlScott deleted the T2687-fix-traverseMirAggregate-bug branch October 8, 2025 01:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-mir-comp Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp
Projects
None yet
Development

Successfully merging this pull request may close these issues.

crux-mir-comp: Panic when clobbering static of type closure [] (traverseMirAggregate: mismatched keys in aggregate)
3 participants