Repository navigation
IR-598: require symbolic V2 replacement before corpus retirement - #358
Merged
Merged
Conversation
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.
The current bounded Kani corpus still evaluates concrete inputs and returns a generation-time
KaniOutcome. AD-004 previously made QSL-353's emission-to-admission coverage sound like sufficient grounds to retire that public path, even though the symbolic V2 replacement and typed graph population input are not yet present.This spec change makes retirement conditional on QSL-emitted packages admitted by Contract IR serving arithmetic, collection and graph cases through the one V2 generator; collection and graph must meet FR-015-AC-96 through AC-102, and proof-eligible cases must use the shared
HarnessSpec/render.rscover rule. Cases without symbolic input do not emit proof harnesses. Generation supplies no proof verdict after replacement; FR-017's installed-backend run does. FR-015, TC-023, interface-001 and AD-004 now state the same boundary. The current corpus contract stays interim until those prerequisites are met.The spec review found two inconsistencies: an AD-004 layout row still named QSL-353 alone, and TC-023 misstated AC-94 trace coverage. Both are fixed on this branch. Eight validated review artifacts (SR-8100 through SR-8107), including dispositions, are included.
Validation:
quire validatefor the changed artifacts andmake specpass on the final head. The full spec gate reports only the existing FR-017 EARS warnings. No code tests were run for this spec-only change. A fresh QSL fetch was unavailable due DNS; the QSL-353 source inspection used cached QSLorigin/main(bdf259f0).