feat: #[non_exhaustive] on the public term enums + variant-addition policy (#104) - #105
Merged
Conversation
…olicy (#104) BvTerm and BoolTerm (asked), plus the sliver's growing term enums (ArrayTerm/ExtBvTerm/ExtOp/ExtBoolTerm — identical failure mode, loom consumes them and they grew once already with symbolic arrays). Adding a variant is no longer a downstream build break — it broke synth twice on BvTerm::Urem, both times via automated dependency updates. CheckResult is DELIBERATELY not marked: a new verdict kind SHOULD break a verification consumer's build — an unhandled verdict falling into a catch-all is exactly the silent-soundness hazard synth's issue names. One correction to the issue's premise, verified on stable rustc: the `non_exhaustive_omitted_patterns` opt-back-in lint is NIGHTLY-ONLY ("unknown lint" on stable). So the CHANGELOG-callout half of synth's proposal is load-bearing, not a nicety — adopted as documented policy on the enum: every variant addition gets a "New BvTerm/BoolTerm variant" changelog heading, and internal matches stay exhaustive (the attribute binds only across crate boundaries; adding an op still forces every in-crate site to handle it — verified: 181 tests compile unchanged). NOTE: applying #[non_exhaustive] is itself a one-time downstream break (consumers must add `_ =>` arms once), so this ships in v0.17.0, a minor — not a patch. Fixes: #104 Trace: skip Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #104 (synth:
BvTerm::Urembroke their exhaustive matches twice, both via automated dependency updates).What's marked
BvTerm,BoolTerm(as asked) — plus the sliver's growing term enums (ArrayTerm/ExtBvTerm/ExtOp/ExtBoolTerm): identical failure mode, loom consumes them, and they grew once already with symbolic arrays.CheckResultis deliberately not marked: a new verdict kind should break a verification consumer's build — an unhandled verdict in a catch-all is exactly the silent-soundness hazard the issue itself names.One premise corrected (verified on stable rustc)
The
non_exhaustive_omitted_patternsopt-back-in lint is nightly-only (unknown linton stable). So the changelog-callout half of synth's proposal is load-bearing, not a nicety — adopted as documented policy on the enum docs: every variant addition gets a "NewBvTerm/BoolTermvariant" changelog heading.Internal soundness pressure preserved
The attribute binds only across crate boundaries: ordeal's own matches (evaluator, blaster, canonicalizer, oracle) stay exhaustive, so adding an op still forces every in-crate site to handle it. Verified — 181 tests compile unchanged.
Versioning note
Applying
#[non_exhaustive]is itself a one-time downstream break (consumers add_ =>arms once), so this ships in v0.17.0, a minor — not a patch.🤖 Generated with Claude Code
https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1